A Programmer Friendly Modular Definition of the Semantics of Java (Extended Abstract)

Egon Borger 1 and Wolfram Schulte 2 1 Universit`a di Pisa, Dipartimento di Informatica, I-56125 Pisa, Italy Email: boerger@di.unipi.it 2 Universitat Ulm, Fakultat fur Informatik, D-89069 Ulm, Germany Email: wolfram@informatik.uni-ulm.de 1 Introduction Java is a general purpose, concurrent, class based, object-oriented language. It is described in the language reference manual [9] (LRM), which gives a description of the meaning of each programming construct of the language. This gives the programmer enough understanding for many purposes, but it is not adequate for use by an implementor or by someone who wants to design his program with mathematical rigor. Thus, a mathematical description of Java is needed. Our goal is to develop a provably correct compiling specification -- using the techniques developed by Borger, Durdanovic and Rosenzweig [5, 2] -- for the compilation of Java programs on the Java virtual machine [13] (VM). The correctness proof of such a compiling specificatio..