language: en

Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation ?

Egon Borger 1 and Wolfram Schulte 2
1 Universita di Pisa, Dipartimento di Informatica,
I-56125 Pisa, Italy
boerger@di.unipi.it
2 Universitat Ulm, Fakultat fur Informatik,
D-89069 Ulm, Germany
wolfram@informatik.uni-ulm.de

Abstract. We provide concise abstract code for running the Java Virtual Machine (JVM) to execute compiled Java programs, and define a general compilation scheme of Java programs to JVM code. These definitions, together with the definition of an abstract interpreter of Java programs given in our previous work [3], allow us to prove that any compiler that satisfies the conditions stated in this paper compiles Java code correctly. In addition we have validated our JVM and compiler specification through experimentation. The modularity of our definitions for Java, the JVM and the compilation scheme exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design-for-reuse. As a by-product we provide a challenging realistic case study for mechanical verification of a compiler correctness proof.

1 Introduction