Advertisement

Correctness of the compiler

  • Robert F. Stärk
  • Joachim Schmid
  • Egon Börger
Chapter

Abstract

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. 1.

    If mn, then σ(m)≤ σ (n)

     
  2. 2.

    The nth state in the run of the Java ε program is equivalent to state σ(n)in the run of the compiled JVM ε program

     

Keywords

Induction 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Robert F. Stärk
    • 1
  • Joachim Schmid
    • 2
  • Egon Börger
    • 3
  1. 1.Theoretische InformatikETH ZentrumZürichSwitzerland
  2. 2.Siemens AGMünchenGermany
  3. 3.Dipartimento di InformaticaUniversità di PisaPisaItaly

Personalised recommendations