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

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 def, 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

• Type: Conference
• Year: 1998
• Where: MFCS
• Authors: Egon Börger, Wolfram Schulte
• Keywords: Compilation Scheme, Compiler, Java Programs, MFCS 1998, Theoretical Computer Science