Jbook Home Page

July 2001

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 AsmGofer and 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 Formalizing 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 implementation.

The authors of Jbook

R.Staerk	(Theoretische Informatik, ETH Zürich)
J.Schmid	(Siemens Corporate Technology, Munich)
E. Börger	(Dipartimento di Informatica Università di Pisa)

The book can be ordered from Springer (Germany), Springer (New York), Amazon (United States), Amazon (Germany), Amazon (United Kingdom), Barnes & Nobles (USA).

Documentation

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 misunderstandings.
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

Definition

Java and the JVM in a Nutshell lists the main rules and functions which constitute the ASM models of Java and the JVM. These rules appear in the appendix of Jbook.

Verification

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 this page.

Validation

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 precompiled binaries for Linux, Solaris Sparc, and cygwin under Microsoft Windows. In addition AsmGofer.tar.gz contains 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

The introduction and the contents of Jbook give a more detailed impression about the topics treated by the book.

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 Robert Stärk.

Survey Lecture on Modeling and Analysis of Java (PowerPoint animation SurveyJava.ppt) by Egon Börger.

Survey Lecture on Modeling and Analysis of JVM (PowerPoint animation SurveyJVM.ppt) by Egon Börger.

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 site.

Downloading Jbook

Jbook-1.04.exe: 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.
machines-1.04.zip: 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.
machines-1.04.tar.gz: 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.
AsmGofer.tar.gz: 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 Jbook-1.04.exe already contains the binary for Microsoft Windows.

Trademarks

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.

ETH Home

July 2001
Responsible