Over the last several months Computational Logic, Inc. (CLI) in collaboration with Schlumberger Electronic Transactions and JavaSoft (see "Where is JavaSoft going with its model" in the original Javasoft announcement) has been building a formal model of a subset of the Java Virtual Machine (JVM). The model has been built using ACL2, a mathematical logic based on Common Lisp. The result can serve as the basis for rigorous, formal analysis of the JVM and JVM (bytecode) programs. Because models written in ACL2 can be executed, the formal JVM model can run programs within the subset of the JVM supported.
The model is called the "defensive" JVM (or dJVM) because it includes sufficient run-time checks to assure type-safe execution (or at least to detect and prevent any unsafe execution). In the standard JVM these checks are not present; type safety is dependent an unstated property of the bytecode verifier and the JVM.
The first phase of the CLI effort has been to build an initial model of a significant portion of the Java Card subset of the JVM. This includes object creation, field access, and method invocation. This phase has been completed, and CLI and its collaborators are making the "alpha" release of the initial model publicly available for external review and comment. This snapshot demonstrates one approach to formalizing and clarifying the JVM specification.
NOTE: The HTML version was generated mechanically from LaTeX sources generated mechanically from the ACL2 source files. While this has produced a readable hyper-linked rendition, there are a number of minor formatting glitches. For the authoritative documentation see the report.
The model is available as gzipped or compressed TAR files which include an executable image and the dJVM 0.5 User's Guide in PostScript and PDF formats:
WARNING: The current executable images are very large; they are approximately 70MB each when expanded. The gzipped versions are about 30 MB. The image includes the executable dJVM model as well as the complete ACL2 theorem prover, compiler, and all of the definitions and theorems of the dJVM model.
The User's Guide briefly explains how to run the model and is available as a postscript or pdf file. The ACL2 source files comprising the model are also available as a gzipped tar file (300KB) .
Java, Java Card and Solaris are trademarks of Sun Microsystems, Inc. SPARC is a trademark of SPARC International, Inc.