Java and the Java Virtual Machine (R. Stärk, J. Schmid, E. Börger)

Some Theorems proved in Jbook

Java is type safe
Type safety means that when a legal, well-typed Java program is executed on the ASM described in Part I of the book, then its state is always in good shape; local variables, class variables, instance fields and array elements always contain values of the declared types; references to objects are always defined in the heap (there are no dangling pointers); expressions are evaluated to values of the compile-time type; even when exceptions are thrown and later caught.

Correctness of the compiler
Every compiler that satisfies the conditions listed in Part II of the book compiles Java programs correctly into JVM code.

Completeness of the compiler
Bytecode generated by the compiler-ASM of Part II from a correct Java program does have type assignments.

Soundness of type assignments
The defensive Virtual Machine in Part II checks the dynamic constraints at run-time. A bytecode type assigment implies that the defensive Virtual Machine executes the code without violating any run-time check.

Soundness of the verifier
For each method in the class environment, the verifier-ASM either computes a bytecode type assignment or terminates with a VerifyError.

Completeness of the verifier
If a method has a type assignment, then the verifier-ASM finds a most specific type assignment and no VerifyError will occur.

ETH Home March 2001
ETH Logo