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

This theorem is proved by straightforward symbolic evaluation, i.e., the repeated
unfolding of the denition of tjvm , together with Boolean and arithmetic sim-
plication.
Once proved, how is this theorem used? Suppose the ACL2 rewriter encoun-
ters a call of tjvm in which the second argument is an inBox-clock expression.
(Previously proved rules about tjvm will insure that arithmetic combinations
of such expressions are decomposed into appropriate nests of tjvm expressions
applied to these clock functions.) Then the rewriter tries to establish that the
next-inst of the TJVM state is an invokevirtual of "inBox" and the resolved
method named "inBox" in the superclass chain of the

object is inBox .
These actions are caused by backchaining. The three hypotheses equating

this

this ,

p 1 ,and p 2 to stack expressions are not restrictive: they are established by bind-

ing p 2 to the corresponding expressions. Provided the hypotheses

are established, the rewriter then replaces the target call of tjvm by a new state
expression in which the program counter is advanced by one, the three actuals of
"inBox" are removed from the stack and the appropriate value is pushed. Thus,
as with our earlier theorem about "fact" , this theorem congures ACL2 to sim-
plify a call of "inBox" almost as though it were a built-in TJVM instruction
whose semantics is given in terms of the Lisp function inBox .
Before proceeding with our presentation we take a slight detour to illustrate
an important but obscure aspect of using ACL2. Readers uninterested in such
details can skip this paragraph. The aspect in question is the fact that ACL2
uses a pattern matcher and backchaining to determine when an equality theorem
is applicable as a rewrite rule. The pattern match is based on the left-hand side
of the concluding equality: when a potential \target term" matching that term
is seen by the rewriter, and the hypotheses can be relieved, the target term is
replaced by the corresponding instance of the right-hand side. So consider the
left-hand side of the conclusion above. Note that `

this , p 1 ,and

s 0 ' occurs twice, once as the
rst argument to tjvm and then again inside the inBox-clock expression. In
actual applications, the expressions in the target term corresponding to these
two occurrences of ` s 0 ' may not be syntactically identical. The rst state is that

in which inBox is being invoked; the second is the state used to compute how
many steps to take. The two states could be syntactically dierent; indeed, they
could be semantically dierent (i.e., not equal). This would prevent a pattern
match and thus prevent the application of the theorem. A logically equivalent
rephrasing of the theorem has the left-hand side (tjvm s 0

k

) and the additional

hypothesis that is equal to (inBox-clock this p 1 p 2 s 0 ) . That is, we do not

need to insist that the clock expression be ` (inBox-clock this p 1 p 2 s 0 ) ', only
that it be an expression with the same value. We follow this line of thinking
just one more step before returning to the main flow of our presentation. If we
rephrase the left-hand side as (tjvm s 0 k ) ACL2 performs slowly because the
pattern now matches every possible call of tjvm and the applicability of the
theorem is entirely dependent on whether the hypotheses can be relieved. In
general, pattern matching is faster than backchaining, so it is wise to put some
syntactic \hint" in the pattern that the theorem applies to an invocation of

k