Java and the Java Virtual Machine Definition, Verification, Validation

Java and the Java Virtual Machine Definition, Verification, Validation / by Robert F. Stärk, Joachim Schmid, Egon Börger.

This book provides a high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is struc...

Full description

Saved in:
Bibliographic Details
Main Authors: Stärk, Robert F. (Author), Schmid, Joachim (Author), Börger, Egon (Author)
Corporate Author: SpringerLink (Online service)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.
Edition:1st ed. 2001.
Series:Springer eBook Collection.
Subjects:
Computer programming.
Programming languages (Electronic computers).
Software engineering.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • 1. Introduction
  • 1.1 The goals of the book
  • 1.2 The contents of the book
  • 1.3 Decomposing Java and the JVM
  • 1.4 Sources and literature
  • 2. Abstract State Machines
  • 2.1 ASMs in a nutshell
  • 2.2 Mathematical definition of ASMs
  • 2.3 Notational conventions
  • I. Java
  • 3. The imperative core JavaI of Java
  • 4. The procedural extension JavaC of JavaI
  • 5. The object-oriented extension $${ text{Jav}}{{ text{a}}_ mathcal{O}}$$ of JavaC
  • 6. The exception-handling extension Java? of $${ text{Jav}}{{ text{a}}_ mathcal{O}}$$
  • 7. The concurrent extension JavaT of Java?
  • 8. Java is type safe
  • II. Compilation of Java: The Trustful JVM
  • 9. The JVMI submachine
  • 10. The procedural extension JVMC of JVMI
  • 11. The object-oriented extension $${ text{JV}}{{ text{M}}_ mathcal{O}}$$ of JVMC
  • 12. The exception-handling extension JVM? of $${ text{JV}}{{ text{M}}_ mathcal{O}}$$
  • 13. Executing the JVMN
  • 14. Correctness of the compiler
  • III. Bytecode Verification: The Secure JVM
  • 15. The defensive virtual machine
  • 16. Bytecode type assignments
  • 17. The diligent virtual machine
  • 18. The dynamic virtual machine
  • A. Executable Models
  • A.1 Overview
  • A.2 Java
  • A.3 Compiler
  • A.4 Java Virtual Machine
  • B. Java
  • B.1 Rules
  • B.2 Arrays
  • C. JVM
  • C.1 Trustful execution
  • C.2 Defensive execution
  • C.3 Diligent execution
  • C.4 Check functions
  • C.5 Successor functions
  • C.6 Constraints
  • C.7 Arrays
  • C.8 Abstract versus real instructions
  • D. Compiler
  • D.1 Compilation functions
  • D.2 maxOpd
  • D.3 Arrays
  • References
  • List of Figures
  • List of Tables.

Similar Items