Joachim Schmid, and Egon Börger, Java
and the Java Virtual Machine: Definition, Verification, Validation.
||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 structured into language layers and
machine components. It comes with a natural executable refinement
(written in AsmGofer and provided on CD-ROM) which can be used for
||Java, Compiler Correctness,
||May be purchased from
Springer-Verlag. Additional material (slides, table of contents,
errata, etc.) can be found at the
Jbook website at
"The Jbook gives the most comprehensive and consistent formal account
of the combination of Java and the JVM." (Pieter Hartel and Luc Moreau
in ACM Computing Surveys 2001,
"Formalizing the Safety of Java, the Java Virtual Machine and Java Card"
, Section 6.2).