In this chapter we formulate and prove the correctness of the compiler for Java ε programs. The goal of the chapter is to show that the run of the ASM for a Java ε program is equivalent to the corresponding run of the JVM ε for the compiled program, based upon a precise definition of the equivalence between a Java ε run and its implementation by a JVM ε run. For example, the run of the Java ε program is finite if and only if the run of the compiled JVM ε program is finite. The correspondence of states to be compared in the two runs will be made explicit by a mapping n ↦ σ(n)with the following properties:
If m ≤ n, then σ(m)≤ σ (n)
The nth state in the run of the Java ε program is equivalent to state σ(n)in the run of the compiled JVM ε program
KeywordsInduction Hypothesis Integrity Constraint Boolean Expression Correctness Proof Return Address
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Unable to display preview. Download preview PDF.
© Springer-Verlag Berlin Heidelberg 2001