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

s 0 :
(make-state
(push (make-frame 0
nil
nil
'((push 5)
(invokestatic "Math" "fact" 1)
(halt)))

nil)

nil
'( Math-class ))

This state is poised to execute the three instruction program above, starting
with the (push 5) at program counter 0. Note that the program pushes 5 on
the stack and then invokes "fact" . The class table for the state includes our
Math-class ,so "fact" , here, means the byte code given in Fact .
The Lisp expression (top (stack (top-frame (tjvm s 0 52)))) steps s 0
52 times, and then recovers the topmost item on the operand stack of the topmost
frame of the call stack. Evaluating this expression produces 120, which is indeed
5!.

How did we know to take 52 steps? The answer is: by analysis of the code
in Fact . The following function, which we call the \clock function" for "fact" ,
returns the number of TJVM instructions required to execute (invokestatic
"Math" "fact" 1) on

n . The function was written based on an inspection of

thebytecodein Fact .

(defun fact-clock ( n )
(if (zp n )
5
(++ 7
(fact-clock (- n 1))
2)))

Here, ++ is just the normal arithmetic addition function. Fact-clock has been
written this way (rather than 5 + 9 ) to make it obvious how such functions

are generated. To execute a call of "fact" on 5 evidently takes 50 TJVM cycles
(including the call ). Thus, the program in s 0 takes 52 cycles.

n

3 Proofs About TJVM Programs

Of more interest than mere execution is the following theorem we can prove
about "fact" .

Theorem. "fact" is correct:
Suppose s 0 is a TJVM state whose next instruction is (invokestatic

"Math" "fact" 1) , where the meaning of the name "Math" in the class
table is our Math-class . Let n be the top of the operand stack in the