Java and the Java Virtual Machine Definition, Verification, Validati
This book provides a high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier c
- PDF / 28,744,808 Bytes
- 375 Pages / 439.37 x 666.142 pts Page_size
- 34 Downloads / 230 Views
Springer Berlin Heidelberg New York Barcelona Hong Kong London Milan Paris Singapore Tokyo
Robert F. SHirk Joachim Schmid Egon Borger
Java and the Java Virtual Machine Definition, Verification, Validation
With 84 Figures, 18 Tables, and CD-ROM
,
Springer
Additional material to this book can be downloaded from http://extras.springer.com
Preface
The origin of this book goes back to the Dagstuhl seminar on Logic for System Engineering, organized during the first week of March 1997 by S. Jiihnichen, J. Loeckx, and M. Wirsing. During that seminar, after Egon Borger's talk on How to Use Abstract State Machines in Software Engineering, Wolfram Schulte, at the time a research assistant at the University of Ulm, Germany, questioned whether ASMs provide anything special as a scientifically wellfounded and rigorous yet simple and industrially viable framework for highlevel design and analysis of complex systems, and for natural refinements of models to executable code. Wolfram Schulte argued, referring to his work with K. Achatz on A Formal Object-Oriented Method Inspired by Fusion and Object-Z [1], that with current techniques of functional programming and of axiomatic specification, one can achieve the same result. An intensive and long debate arose from this discussion. At the end of the week, it led Egon Borger to propose a collaboration on a real-life specification project of Wolfram Schulte's choice, as a comparative field test of purely functionaldeclarative methods and of their enhancement within an integrated abstract state-based operational (ASM) approach. After some hesitation, in May 1997 Wolfram Schulte accepted the offer and chose as the theme a high-level specification of Java and of the Java Virtual Machine. What followed were two years of hard but enjoyable joint work, resulting in a series of ASM models of the Java language, of the JVM, and of a provably correct compilation scheme for compiling Java programs to JVM code, which were published in [9, 8, 10, 11, 12]. When in the spring of 1999, Wolfram Schulte put this work together for his Habilitationsschrift at the University of Ulm, Egon Borger suggested completing and extending it to a-badly needed- full-blown ASM case study book. The book should show the ASM method at work, convincingly, for the practical design of a complex real-life system, and for its rigorous mathematical and extensive experimental analysis. Robert Stark and Joachim Schmid accepted to join this book project. At that time, in his Fribourg lectures [33], Robert Stark had already elaborated part of the Java-to-JVM compilation correctness claim, namely, that the execution, on the ASM for the JVM, of every correctly compiled legal Java program is equivalent to the execution of the original Java program
VI
Preface
on the ASM for Java. In the spring of 1998, Egon Borger had proposed to Joachim Schmid a PhD thesis, hosted by Siemens Corporate Technology in Munich, on defining and implementing practically useful structuring and decomposition principles for large ASMs. It could
