Skip to main content
main-content

Über dieses Buch

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 well­ founded and rigorous yet simple and industrially viable framework for high­ level 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 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.

Inhaltsverzeichnis

Frontmatter

Introduction

1. Introduction

Abstract
This book provides a structured and high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including the standard compilation of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into modules (language layers and machine components), and its abstract character implies that it is truly platform-independent. It comes with a natural refinement to executable machines on which code can be tested, exploiting in particular the potential of model-based high-level testing. The analysis brings to light in what sense, and under which conditions, legal Java programs can be guaranteed to be correctly compiled, to successfully pass the bytecode verifier, and to be executed on the JVM correctly, i.e., faithfully reflecting the Java semantics and without violating any run-time checks. The method we develop for this purpose, using Abstract State Machines which one may view as code written in an abstract programming language, can be applied to other virtual machines and to other programming languages as well.
Robert F. Stärk, Joachim Schmid, Egon Börger

Abstract State Machine

2. Abstract State Machines

Abstract
The notion of Abstract State Machines (ASMs), defined in [20], captures in mathematically rigorous yet transparent form some fundamental operational intuitions of computing, and the notation is familiar from programming practice and mathematical standards. This allows the practitioner to work with ASMs without any further explanation, viewing them as `pseudocode over abstract data’ which comes with a well defined semantics supporting the intuitive understanding. We therefore suggest to skip this chapter and to come back to it only should the need be felt upon further reading.
Robert F. Stärk, Joachim Schmid, Egon Börger

Java

Frontmatter

3. The imperative core Java I of Java

Abstract
In this chapter we define the basic model execJava I , which defines the semantics of the sequential imperative core of Java with statements (appearing in method bodies) and expressions (appearing in statements) over the primitive types of Java. Each machine is started with an arbitrary but fixed Java program it has to interpret. In Sect. 3.1 we describe the signature of Java I and the static semantics of the input programs. We explain the form in which these programs are supposed to appear to the ASM, namely as annotated abstract syntax trees, resulting from parsing and elaboration. For future use in the proofs we also list the constraints which are imposed on the syntax of programs and on the types of the constructs appearing in them. In Sect. 3.2 we define the ASM rules for the dynamic semantics of \({\text{Jav}}{{\text{a}}_\mathcal{I}}\) programs.
Robert F. Stärk, Joachim Schmid, Egon Börger

4. The procedural extension Java C of Java I

Abstract
Java c extends Java I by classes and interfaces, more precisely by class fields, class methods and class initializers, also called static fields, static methods and static initializers. Classes play the role of modules: class variables correspond to global variables, class methods to procedures (also called subroutines or functions) and class initializers to module initializers. In Sect. 4.1 we describe the static and in Sect. 4.2 the dynamic part of the semantics of Java c .
Robert F. Stärk, Joachim Schmid, Egon Börger

5. The object-oriented extension of Java c

Abstract
\({\text{Jav}}{{\text{a}}_\mathcal{O}}\) extends Java c to an object-oriented language, supporting the following new features to form expressions: instance fields, instance methods, creation of new instances, method overriding, type casts, type checks and null pointers. Correspondingly execJava O introduces new rules for expression evaluation and handling of values. In Sect. 5.1 we describe the static and in Sect. 5.2 the dynamic part of the semantics of \({\text{Jav}}{{\text{a}}_\mathcal{O}}\).
Robert F. Stärk, Joachim Schmid, Egon Börger

6. The exception-handling extension Java ε of

Abstract
Java ε extends \({\text{Jav}}{{\text{a}}_\mathcal{O}}\) with exceptions, designed to provide support for recovering from abnormal situations. In this extension of the previous machines it becomes transparent how break and continue statements (in Java I ), return statements (in Java C ) and the initialization of classes and interfaces (in \({\text{Jav}}{{\text{a}}_\mathcal{O}}\)) interact with catching and handling exceptions. When a Java program violates certain semantic constraints at run-time, the JVM signals this error to the program as an exception. The control is transferred, from the point where the exception occurred, to a point that can be specified by the programmer. An exception is said to be thrown from the point where it occurred, and it is said to be caught at the point to which control is transferred. Exceptions are represented in Java by instances of subclasses of the class Throwable. Java distinguishes between run-time exceptions (which correspond to invalid operations violating the semantic constraints of Java, like an attempt to divide by zero or to index an array outside its bounds), errors (which are failures detected by the executing machine), and user-defined exceptions. We consider here only run-time and user-defined exceptions, since errors belong to the JVM and are therefore ignored in the dynamic semantics of Java.
Robert F. Stärk, Joachim Schmid, Egon Börger

7. The concurrent extension Java T of Java ε

Abstract
The abstract state machine execJava defines the behavior of Java executing a single phrase at a time and by a single thread. In this chapter we extend Java ε to Java T so that execJava can be embedded into a machine execJavaThread, for multithreaded Java, which provides support for execution of multiple tasks with shared main and local working memory. We consider the mechanisms Java provides for thread creation and destruction, for synchronizing the concurrent activity of threads using locks, and for waiting and notification introduced for an efficient transfer of control between threads. We describe the methods for starting (start), interrupting (interrupt), suspending (wait),and resuming (notify) threads as normal methods, which for the purpose of executability are included here into native methods.
Robert F. Stärk, Joachim Schmid, Egon Börger

8. Java is type safe

Abstract
In this chapter we analyze and prove some structural properties of Java runs which are needed for the proof that Java is type safe (Theorem 8.4.1), and for the correctness proof of the compilation of Java to JVM bytecode (Chapter 14). This includes the reachability analysis for expressions and statements (Sect. 8.2) and the rules of definite assignment for local variables (Sect. 8.3, where we correct two inconsistencies in the rules defined in the JLS [19]).
Robert F. Stärk, Joachim Schmid, Egon Börger

Compilation of Java: The Trustful JVM

Frontmatter

9. The JVM I submachine

Abstract
In this chapter we define the JVM submachine JVM I which can execute compiled Java I programs. We also define a standard compilation scheme for translating Java I programs to JVM I code.
Robert F. Stärk, Joachim Schmid, Egon Börger

10. The procedural extension JVM C of JVM I

Abstract
In this chapter we extend the machine JVM I to a JVM submachine JVM C which can execute compiled Java c programs. The extension consists in adding rules for handling class variables, and for method invocation and return. We introduce a submachine switchVM C which takes care of frame stack manipulations—upon method invocation or return and upon implicit class initialization—and which will be extended in switchVM E for frame manipulations due to capturing exceptions. We also extend the Java I -to-JVM I compilation scheme by translating the new Javac expressions and statements to JVM C code.
Robert F. Stärk, Joachim Schmid, Egon Börger

11. The object-oriented extension of JVM c

Abstract
In this chapter we extend the machine JVM c to a JVM submachine \({\text{JV}}{{\text{M}}_\mathcal{O}}\) which can execute compiled \({\text{JV}}{{\text{M}}_\mathcal{O}}\) programs. We also extend the Java C -to JVM c compilation scheme by translating the new \({\text{JV}}{{\text{M}}_\mathcal{O}}\) expressions and statements to \({\text{JV}}{{\text{M}}_\mathcal{O}}\) code.
Robert F. Stärk, Joachim Schmid, Egon Börger

12. The exception-handling extension JVM ε of

Abstract
In this chapter we extend the machine \({\text{JV}}{{\text{M}}_\mathcal{O}}\) to a JVM submachine JVM ε which can execute compiled Java ε programs This includes extending the submachine switchVM C to switchVM E which copes with frame stack manipulations due to exception handling. We also extend the \({\text{JV}}{{\text{M}}_\mathcal{O}}\)-to— \({\text{JV}}{{\text{M}}_\mathcal{O}}\) compilation scheme by translating the new Java ε statements to JVM ε code.
Robert F. Stärk, Joachim Schmid, Egon Börger

13. Executing the JVM N

Abstract
The specification of the Java Virtual Machine is not complete without the specification of all native methods which are used in the JDK libraries. Unfortunately, not all native methods are described in the official specifications. Therefore, one is constrained to using Sun’s JVM if one wants to use Sun’s JDK libraries.
Robert F. Stärk, Joachim Schmid, Egon Börger

14. Correctness of the compiler

Abstract
In this chapter we formulate and prove the correctness of the compiler for Java ε programs. The goal of the chapter is to show that the run of the ASM for a Java ε program is equivalent to the corresponding run of the JVM ε for the compiled program, based upon a precise definition of the equivalence between a Java ε run and its implementation by a JVM ε run. For example, the run of the Java ε program is finite if and only if the run of the compiled JVM ε program is finite. The correspondence of states to be compared in the two runs will be made explicit by a mapping nσ(n)with the following properties:
1.
If mn, then σ(m)≤ σ (n)
 
2.
The nth state in the run of the Java ε program is equivalent to state σ(n)in the run of the compiled JVM ε program
 
Robert F. Stärk, Joachim Schmid, Egon Börger

Bytecode Verification: The Secure JVM

Frontmatter

15. The defensive virtual machine

Abstract
In this chapter we lift the trustfully executing machine of Part II to a defensive machine which checks each instruction before its execution to satisfy certain constraints about types, resource bounds, etc., guaranteeing correct execution in such a way that if the defensive VM executes bytecode successfully, then also the trustful VM does so with the same semantical effect. Our goal here is to prepare the description of the bytecode verifier, to be given in the next chapters, by a transparent definition of the verification functionality, namely in terms of run-time checks of the safe executability of single instructions. We formulate these checking conditions in terms of the types of values instead of values themselves so that they can be adapted in the next two chapters to link-time verifiable properties.
Robert F. Stärk, Joachim Schmid, Egon Börger

16. Bytecode type assignments

Abstract
In this chapter we analyze the dynamic constraints, which are checked at run-time by the defensive VM, to extract from them link-time checkable conditions on bytecode which, if satisfied, imply that the defensive VM executes the code without violating any run-time check (Soundness Theorem 16.4.1 for bytecode type assignments). We refine the compilation function of Part II by an appropriate type frame, which is associated to every instruction, and show that code, if generated from a correct Java program and following this certifying compilation scheme, does satisfy these link-time checkable bytecode conditions (Compiler Completeness Theorem 16.5.2 for bytecode type assignments). In the next chapter we will show that for a large class of programs bytecode type assignments can be computed using a fixed point computation.
Robert F. Stärk, Joachim Schmid, Egon Börger

17. The diligent virtual machine

Abstract
In this chapter we distill from the incrementally defined defensive machine the analogously stepwise refined diligent virtual machine. It combines the trustful machine of Part II with a link-time bytecode verifier. We prove (Theorem 17.1.1) that this verifier is sound, i.e., that for each method in the class environment, the verifier either computes a bytecode type assignment in the sense of Chapter 16 or terminates with a VerifyError. We also prove (Theorem 17.1.2) the completeness of the verifier, i.e., that a) if there exists a bytecode type assignment for the body of a method, then the bytecode verifier computes a principal (most specific) type assignment; b) if the body of a method is not typeable, then the bytecode verifier returns a VerifyError. By the soundness of bytecode type assignments (Theorem 16.4.1) it follows that, if the bytecode verifier is successful, then the run-time checks of the defensive VM of Chapter 15 are always satisfied thus establishing the Main Theorem of this book.
Robert F. Stärk, Joachim Schmid, Egon Börger

18. The dynamic virtual machine

Abstract
In this chapter we refine the virtual machines of the previous chapters to a dynamic machine that incorporates dynamic loading and linking of classes. This involves new rules for class loader methods and an extension of switch VM E to switch VM D to cope with referencing loaded classes (together with their superclasses) before they are linked.
Robert F. Stärk, Joachim Schmid, Egon Börger

Backmatter

Weitere Informationen