javacand then proving the corresponding theorem about the JVM. Certain automatically applied strategies are implemented with rewrite rules (and other proof-guiding pragmas) in ACL2 ``books'' to control the theorem prover when operating on problems involving the JVM model.
apprentice-state.lisp-- the Apprentice initial state (4 KB)
apprentice.lisp-- the Apprentice proof script (97 KB)
certify.lisp-- a script to re-certify all these files (4 KB)
demo.lisp-- a proof script for the Java recursive factorial method (20 KB)
isort.lisp-- a proof script for the Java insertion sort method (38 KB)
iterativedemo.lisp-- a proof script for the Java iterative factorial method (9 KB)
m5.lisp-- the M5 JVM model (101 KB)
perm.lisp-- some lemmas about permutations (1 KB)
universal.lisp-- a proof script for the ``universal program'' that can return any
utilities.lisp-- basic M5 utility lemmas (5 KB)
utilities.lisp. In them you will find
include-bookcommands that mention the standard books
books/ihs/quotient-remainder-lemmas. Change these pathnames to those for your machine.
Then, while connected to the directory on which you downloaded the files,
fire up ACL2 and execute
(ld "certify.lisp" :ld-pre-eval-print t).
Recertification takes just a few minutes for all but the
example. That one takes about 2 hours.