Springer-Verlag Java and the Java Virtual Machine.pdf

Robert St¨ark,Joachim Schmid, Egon er
Java and the
Java Virtual Machine
Definition, Verification, Validation
May 8, 2001
Springer-Verlag
Berlin Heidelberg NewYork
London Paris Tokyo
Hong Kong Barcelona
Budapest
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. J¨ahnichen,
J. Loeckx, and M. Wirsing. During that seminar, after Egon er’stalk
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 well-
founded and rigorous yet simple and industrially viable framework for high-
level design and analysis plex 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 erto propose a collaboration on a real-life specification project of
Wolfram Schulte’s choice, as parative field test of purely functional-
declarative 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 pilation scheme piling 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 p