Proving Theorems about Java-like Byte Code
J Strother Moore
Abstract
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.
- full paper
tjvm.lisp: This script corresponds to the section of the
paper `Specification of the TJVM'.
examples.lisp: This script contains all the lemmas and
theorems mentioned in the paper.
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.