Information Technology Reference
In-Depth Information
topmost frame of the call stack of
s
0
and suppose
n
is a natural number.
Then the TJVM state obtained by stepping
s
0
(fact-clock
n
)
times
is state
s
0
with the program counter incremented by one and the
n
on
the operand stack replaced by
n
!. The heap is unchanged.
This informal statement can be phrased formally as follows.
Theorem.
"fact"
is correct:
(implies (and (equal (next-inst
s
0
)
'(invokestatic "Math" "fact" 1))
(equal (assoc-equal "Math" (class-table
s
0
))
Math-class
)
(equal
n
(top (stack (top-frame
s
0
))))
(natp
n
))
(equal
(tjvm
s
0
(fact-clock
n
))
(make-state
(push (make-frame (+ 1 (pc (top-frame
s
0
)))
(locals (top-frame
s
0
))
(push (fact
n
)
(pop (stack (top-frame
s
0
))))
(program (top-frame
s
0
)))
(pop (call-stack
s
0
)))
(heap
s
0
)
(class-table
s
0
))))
The theorem states the
total correctness
of the
"fact"
byte code. Weaker the-
orems can be stated and proved, but we here focus on theorems of this kind
because they are easiest to prove.
We proved this theorem in a very straightforward manner using ACL2. The
proof takes 0.33 seconds on a 200 MHz Sun Ultra 2. The theorem only looks
complicated because the notation is unfamiliar!
ACL2 is an automatic theorem prover in the sense that its behavior on any
given proof attempt is determined by its state immediately prior to the attempt,
together with goal-specic hints provided by the user. Of great importance is
the set of lemmas the system has already proved. Those lemmas determine how
ACL2 simplies expressions. To congure ACL2 to prove theorems about TJVM
we followed the example described in [3]. Roughly speaking, we did the following:
{
We proved half a dozen simple arithmetic lemmas; we could have loaded any
of several standard ACL2 arithmetic \books."
{
We proved lemmas that let ACL2 manipulate the data structures used on
the TJVM, including stacks, frames, and states, as abstract data structures.
One such theorem is
(top (push
x stack
))
=
. We then \disabled" the
denitions of the primitive stack, frame, and state functions so that their
\implementations" in terms of conses were not visible.
{
We proved the standard theorem for expanding the single step function,
step
, when the
next-inst
is explicit. We then disabled the step function.
This prevents case explosion on what the next instruction is.
x
Search WWH ::
Custom Search