Jbook Home Page
Java and the Java Virtual Machine
— Definition, Verification, Validation|
The 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 structured into language layers and machine components.
It comes with a natural executable refinement (written in
provided on CD-ROM) which can be used for testing code. The method
developed for this purpose, using
Abstract State Machines
(ASMs), can be applied to other virtual machines and to other
programming languages as well.
The Jbook gives the most comprehensive and consistent formal
account of the combination of Java and the JVM.
(Pieter Hartel and Luc Moreau in
the Safety of Java, the Java Virtual Machine and Java Card,
ACM Computing Surveys, 33(4):517-558, 2001. Section 6.2, page 540.)
The target readers are practitioners—programmers, implementors,
standardizers, lecturers, students—who need for their work a complete,
and at the same time transparent definition, and an executable model, of
the language, and of the virtual machine underlying its intended
The authors of Jbook
|| (Theoretische Informatik, ETH Zürich)|
||(Siemens Corporate Technology, Munich) |
||(Dipartimento di Informatica Università di Pisa)
The book can be ordered from
Amazon (United States),
Amazon (United Kingdom),
Barnes & Nobles (USA).
- About Jbook
- Describes what the Jbook offers for which group of readers.
- What's New
- Describes changes of the web pages.
- Jbook FAQ
- Gives email feedback on Jbook and tries to clarify
- Jbook Updates
- Gives information about known errata and errors in the Jbook
and in the executable models. Describes how you can
communicate to the authors should you discover a new error.
Some highlights of Jbook
The introduction and the
contents of Jbook give a
more detailed impression about the topics treated by the book.
- Java and the JVM in a Nutshell
the main rules and functions which constitute the ASM
models of Java and the JVM. These rules appear in the
appendix of Jbook.
- We analyse and prove the following fundamental property of JVM
verification and execution of compiled Java programs:
Under explicitly stated conditions, any well-formed and well-typed
Java program, when correctly compiled,
passes the verifier and is executed on the JVM. It executes
without violating any run-time checks, and is correct with
respect to the expected behavior as defined by the Java machine.
The proof for this fundamental property uses several other
theorems. Some of them are described on
- The book comes with an electronic version on CD-ROM which
includes the executable versions of the models, with examples
and exercises described in the book. It comes with a
setup program Jbook-1.04.exe
for Microsoft Windows based platforms and
for Linux, Solaris Sparc, and cygwin under
Microsoft Windows. In addition
the source code of AsmGofer,
which is the tool used to execute the
models in the book. You will need the sources only in case you have to
compile your own binary of AsmGofer. The setup program
Jbook-1.04.exe already contains the
binary for Microsoft Windows.
- Some legal Java
programs are not bytecode verifiable
- Bugs in Verifiers
Material about Jbook
Copyright Notice. The work below is copyright by the respective authors
who reserve all rights to their work. Fair use of the material is
welcome, including using and making the material available for
lecturing. In doing this the source and the authors should be mentioned,
when passing off the material this copyright notice should be added. In
particular, it is not fair to pass off any material
made publicly available here as your own work.
Course Java and the JVM: Definition and Verification
at ETH Zürich by
on Modeling and Analysis of Java
(PowerPoint animation SurveyJava.ppt)
on Modeling and Analysis of JVM
(PowerPoint animation SurveyJVM.ppt)
If you like the book, you are welcome to submit your own teaching or
other material (slides, exercises, etc.) on the book as addition to this
Setup program for Microsoft Windows based
platforms. The program contains the executable models
of the Jbook together with examples and exercises
described in the book.
Zip archive for the executable models of
the Jbook together with examples and exercises
described in the book. The zip file contains
binaries for Microsoft Windows.
Compressed tar archive of the executable models of
the Jbook together with examples and exercises
described in the book. The archive contains precompiled
binaries for Linux, Solaris Sparc,
and cygwin under Microsoft Windows.
- The source code of AsmGofer.
The tool is used to execute the models in the Jbook. You will
need the sources only in case you have to compile your
own binary of AsmGofer. The setup program
contains the binary for Microsoft Windows.
Solaris, Java and all Java-based marks are trademarks or registered
trademarks of Sun Microsystems, Inc. in the United States and
other countries. We are independent of
Sun Microsystems, Inc.
Microsoft Windows is registered trademark of
Microsoft Corporation in the United States and/or other countries.