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

one byte. Finally, the JVM has typed instructions, e.g., the JVM's iload loads
an integer-valued variable on the stack while the TJVM's load loads any value.
When this program is invoked on the TJVM, one actual parameter,

,is
popped from the operand stack of the topmost frame of the TJVM call stack; a
new frame is built and pushed onto the call stack of the TJVM state. The new
frame has program counter 0 and the eleven instructions above as the program.
The locals of the new frame bind n to the actual

n

n

. The operand stack of the

new frame is empty.
The program operates as follows. The parenthesized numbers refer to pro-
gram counter values. (0) The local value, ,of n is pushed onto the operand

stack. (1) The ifle instruction pops the operand stack and compares the item
obtained, here

n

0, the program counter is incremented by 8 ;oth-
erwise it is incremented by 1 . (9-10) In the former case, the program pushes a
1 on the operand stack and returns one result to the caller. The JVM uses a
special, single byte instruction for pushing the constant 1 , while the TJVM has
one general-purpose push instruction for pushing any constant. (2) In the case
that

n ,to0.If n

and
(4) 1 and (5) executing a sub which pops two items o the operand stack and
pushes their dierence), (6) invokes this procedure recursively on one actual, in
this case, the

n> 0, the program pushes n , (3-5) pushes n − 1 (by (3) pushing n

1)!, which is
pushed on the stack in place of the actual, (7) multiplies the top two elements
of the stack, and (8) returns that one result to the caller.
From the above description it should be clear how we dene the semantics of
the instructions illustrated above. For example, here is the function which gives
semantics to the add instruction, (add) .
(defun execute-ADD ( inst s )
(declare (ignore inst ))
(make-state
(push (make-frame (+ 1 (pc (top-frame s )))
(locals (top-frame s ))
(push (+ (top (pop (stack (top-frame s ))))
(top (stack (top-frame s ))))
(pop (pop (stack (top-frame s )))))
(program (top-frame s )))
(pop (call-stack s )))
(heap s )
(class-table s )))
This Lisp function { which in the ACL2 setting is taken as an axiom dening the
expression (execute-ADD inst s ) { takes two arguments, the add instruction
to be interpreted and the TJVM state

n − 1 on the stack, obtaining one result, here ( n −

. Because the TJVM add instruction has
no operands, execute-ADD does not actually need the instruction and so

s

inst

above is ignored. The function computes the state obtained from by executing

an add . The new state contains a modied call stack but the same heap and class
table as

s

. The call stack is modied by changing only its topmost frame so that
the program counter is incremented by one and the operand stack is modied
by popping two items o of it and pushing their sum. The locals and program

s