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

{ We dened the standard \clock addition" function, ++ , which is really just
natural number addition, and disabled it. This allows us to dene clock
function in the structured style illustrated fact-clock and prevents the
arithmetic rules from rearranging the expressions and destroying the struc-
tural \hints" implicit in the denitions. We proved the rules that allow
tjvm expressions to be decomposed according to their clock expressions. For
example, (tjvm s (++ ij )) is rewritten to (tjvm (tjvm si ) j ) .Thus,

when ACL2 encounters, for example, (tjvm n

1)) 2)) it decomposes it into a run of length seven, followed by a run of
length (fact-clock (-

s 0 (++ 7 (fact-clock (-

1)) , followed by a run of length two, and each
run must be fully simplied to a symbolic state before the next can be sim-
plied (because of the way the step function has been limited).
{ Finally we prove the standard \memory management" rules, which in the
case of the TJVM tell us the algebra of association lists (used to bind vari-
ables, associate programs with method names, method names with methods,
elds with their contents, etc.).

n

Having so congured ACL2, the theorem about "fact" above is proved by
giving the theorem prover a single hint, namely to do the induction that unwinds
the code in "fact" .
It is important to realize that the theorem above about "fact" contributes
to the further conguration of ACL2 in this capacity. The theorem causes the
following future behavior of ACL2: Suppose the system encounters an expression
of the form (tjvm (fact-clock )) to simplify. Then it rst determines
whether the next instruction of the state is (invokestatic "Math" "fact"

1) where the meaning of "Math" in

is our Math-class , and whether is on

top of the operand stack of and is a natural number. If so, it replaces (tjvm

)) by the corresponding make-state expression in which the
program counter has been incremented by one and

(fact-clock

has been replaced by (fact

) .

Thus, after this theorem is proved, the theorem prover no longer looks at the
code for "fact" .Itstepsover (invokestatic "Math" "fact" 1) as though it
were a primitive instruction that computes the factorial of the top of the stack.
The verication of a system of methods is no harder than the combined
verication of each method in the system. This remark, while trivial, has pro-
found consequences if one clearly views the software verication problem as the
specication and verication of the component pieces.

4 More Example TJVM Executions

The "fact" method does not aect the heap. That is, it does not create any new
objects or modify existing objects. How does our verication strategy cope with
that? We will consider a simple example of a heap modifying method. But we
rst illustrate such methods by simple execution. Consider the following TJVM
class declaration for a class named "Point" , which extends the "Object" class