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

of the frame are unchanged. We call execute-ADD the semantic function for the
TJVM add instruction.
Each instruction on the TJVM is dened by an analogous semantic function.
The semantic function for the instruction (new " class ") , which constructs a
new instance of the class named " class " , is shown below. The instruction takes
as its single argument the name of a class. On our TJVM, new builds a new,
uninitialized instance of that class, allocating some address in the heap for that
instance and leaving that address on the top of the stack in the top frame of the
call stack.

(defun execute-NEW ( inst s )
(let* (( class (arg1 inst ))
( table (class-table s ))
( obj (build-an-instance
(cons class
(class-decl-superclasses
(bound? class table )))

table ))
( addr (length (heap s ))))
(make-state
(push (make-frame (+ 1 (pc (top-frame s )))
(locals (top-frame s ))
(push (list 'REF addr )
(stack (top-frame s )))
(program (top-frame s )))
(pop (call-stack s )))
(bind addr obj (heap s ))
(class-table s ))))

In the ACL2 denition above, s

is the state to be \modied." The let* in the denition above just binds four
variables and then evaluates the make-state expression in the \body" of the
let* . The rst variable,

inst is the new instruction to be executed, and

class , is bound to the class name in the instruction.

The second variable, . This table

contains a description of all the loaded classes, their elds and their methods.
The third variable,

table , is bound to the class table of the state s

, is the uninitialized instance object constructed by new .
Logically speaking, it is constructed by the ACL2 function build-an-instance
from the superclass chain of

obj

class (starting with class ) and the class table .The

fourth variable, addr is the heap address at which obj will be placed. In the

TJVM, this just the number of objects allocated so far.
The state constructed by execute-NEW above modies the top frame of the
call stack of is unchanged.

In the modied top frame, the program counter is incremented and a reference to
addr

s and also modies the heap of s . The class table of s

is pushed onto the operand stack. (Note that the address is \tagged" with
the symbol REF so that it is possible on the TJVM to distinguish integers from
references to heap addresses.) In the modied heap, the new instance object,
obj , is associated with the address addr .