Proving Theorems about Java-like Byte Code
J Strother Moore


We describe a formalization of an abstract machine very similar to the Java Virtual Machine but far simpler. We develop techniques for specifying the properties of classes and methods for this machine. We develop techniques for mechanically proving theorems about classes and methods. We discuss two such proofs, that of a static method implementing the factorial function and of an instance method that destructively manipulates objects in a way that takes advantage of inheritance. We conclude with a brief discussion of the advantages and disadvantages of this approach. The formalization and proofs are done with the ACL2 theorem proving system.

You should download each of the two script files onto some directory. You may simply read them to see the definitions and theorems.

But if you wish to replay the proofs and inspect the output or experiment with further theorems, you should certify both books with ACL2. Certification directions are included at the top of each file. The directions require that you edit your copy of examples.lisp so that the include-book command at the beginning refers to the full pathname of your copy of tjvm.lisp.