Correctness of the compiler

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: 1.If m ≤ n, then σ(m)≤ σ (n)2.The nth state in the run of the Java _ε program is equivalent to state σ(n)in the run of the compiled JVM _ε program