Proving Theorems About Java-Like Byte Code - Correct System Design: Recent Insights and Advances - page 152

the object of the "setColorBox" invocation, and that object is within the

specied box, then the dereferenced object is the result of setting the "color"
of the same object in the old heap. Otherwise, dereferencing with respect to the
new heap produces the same result as dereferencing with respect to the old heap.
Thus, setColorBox-heap is just a succinct symbolic representation of the heap
produced by "setColorBox" and whenever references arise with respect to it,
they are eliminated and replaced by modied instances obtained through the old
heap.
While we have not illustrated classes that chain instances together or instance
methods that are recursive or iterative, these aspects of the TJVM should raise
no problems not predicted by our handling of the recursive factorial and the
simple instance methods shown. That is not to say that such proofs are trivial,
only that their nature is entirely predictable from what has been shown here.
The expectation is that the ACL2 user able to do the proofs shown would be able
to develop the techniques necessary to do proofs of this more involved nature.

this

6 Conclusion

We have shown how a simple version of the Java Virtual Machine can be formal-
ized in the applicative Common Lisp supported by the ACL2 theorem prover.
We have discussed how ACL2 can be congured to make it straightforward
to reason about static and instance methods, including recursive methods and
methods which modify objects in the heap.
A common criticism of this approach is our use of \clocks." Basically, clocks
arise for a deep logical reason: the function tjvm is inadmissible otherwise be-
cause it is not total. We make tjvm total by limiting the number of instructions.
There are other means, e.g., limiting the stack depth (i.e., method invocation
depth) and imposing some bound or measure on back jumps, or, equipping every
state with a measure establishing termination. These means free the user from
counting instructions, at the expense of counting some other unit of computa-
tion. We personally nd instruction-level clocks conceptually simplest.
Instruction-level clocking provides \little step" operational semantics but al-
lows the proof of lemmas, like those shown here, that provide \big step" seman-
tics for subroutine call. Furthermore, we have shown how the two are naturally
mixed.
Whether one uses instruction-level clocking or some other form of counting,
clock expressions allow the user to structure proofs. Every addend in a ++ -nest
gives rise to a single call of tjvm which must be simplied. Thus, by choice of
an appropriate clock expression one can decompose proofs into the segments
about which one is prepared to reason by specially-tailored lemmas. To the
extent that one can decompose a computation mechanically into such regions,
one can mechanically generate clock expressions to control the proof decompo-
sition. Clock expressions compose in the obvious way with invokevirtual and
invokestatic . Iterative computations are handled similarly.