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 Responsible