We define a formal model of the dJVM using the ACL2 language. Because ACL2 is an executable mathematical logic, we obtain a model which we can run, as well as one about which we can formally reason. This provides both the clarity and proof cababilities of a formal, logical model, and the ability to validate the specification against our intensions by running test cases on the model.
The JVM is an optimized version of the dJVM, which behaves correctly (i.e., as the dJVM) under proper conditions. The Java bytecode verifier is intended to assure those conditions by rejecting bytecode programs that do not satisfy the assumptions underlying the JVM optimizations. The main portion of these assumptions address the type safety of the bytecode program.
Warning to the Reader toc{section}{Warning to the Reader}
This is a draft (or ``alpha'' release) of the dJVM 0.5 specification. It is meant as an exploration of formalizing the Java Virtual Machine, the the completeness of the current JVM documentation, and type-safe execution of the JVM. As such, the emphasis was to build an initial formal model of the core, object-oriented portion of the JVM. The model is called dJVM version 0.5 to suggest that it is only an initial step toward formally modeling the full Java Virtual Machine. The text that accompanies portions of the formal model is (yet) not a full or adequate explanation or justification of the model.
The text is sprinkled with ``author's remarks.'' These notes are indicative that this is an incomplete report of an incomplete model. The remarks are marked in the text as:
Acknowledgments
Thanks to Bill Young, and Mike Smith for help and support during development of the model. Thanks to Marianne Mueller and Li Gong of JavaSoft and Scott Guthery of Schlumberger Electronic Transactions for thinking this work was worth pursuing.
And, of course, thanks to the Java team for creating a pleasing language and virtual machine, which are at once both useful enough to generate net-wide excitement and interest, and clean enough to make a formal definition reasonable (and not nearly as hard as for most other practical programming languages). My main sources of information have been the Java Language Specification by James Gosling, Bill Joy, and Guy Steele, and the Java Virtual Machine Specification by Tim Lindholm and Frank Yellin. These two works have provided examples of clear, readable, quite complete explanations of a subtly-complex programming language and virtual machine. I know that considerable care and effort went into making these works available so early in Java's growth. These two works have been the main sources for building the dJVM model.
Thanks to Sun Microsystems, Inc., for permission to use extensive quotations from the Java Language Specification [JLS] and the Java Virtual Machine Specification [JVMS].
Thanks for Schlumberger, JavaSoft, and CLI for supporting this work.
This report was prepared using Perl and , which alternately made progress a pleasure and a puzzle, and repeatedly reminded the author that programming is a rewarding, complex, exacting, and sometimes inscrutable activity.