Java and the Java Virtual Machine
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
- Completeness of the verifier
- If a method has a type assignment, then the verifier-ASM finds
a most specific type assignment and no VerifyError