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.
Preview
Unable to display preview. Download preview PDF.
References
E. Börger and W. Schulte. Defining the Java Virtual Machine as platform for provably correct Java compilation. Technical report, Universität Ulm, Fakultät für Informatik. Ulm, Germany, 1998.
E. Börger and W. Schulte. A modular design for the Java VM architecture. In E. Börger, editor, Architecture Design and Validation Methods. Springer LNCS, to appear, 1998.
E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java(tm), Springer LNCS, to appear. 1998.
J. Gosling, B. Joy, and G. Steele. The Java(tm) Language Specification. Addison Wesley, 1996.
Y. Gurevich. Evolving algebras 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
T. Lindholm and F. Yellin. The Java(tm) Virtual Machine Specification. Addison Wesley, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E., Schulte, W. (1998). Defining the Java Virtual Machine as platform for provably correct Java compilation. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055755
Download citation
DOI: https://doi.org/10.1007/BFb0055755
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive