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

It then pushes a new frame poised to execute the resolved method, initializing
the locals in the new frame by binding to the items just popped.

Recall that our fact method used the instruction invokestatic . That in-
struction is similar to invokevirtual but does not involve a \this" object. Static
method resolution is based on the class name used in the invokestatic instruc-
tion.
Observe that the class name argument in the invokevirtual instruction is
ignored (the ACL2 function above does not use (arg1 inst ) ). Why is it provided
in the rst place? This is a reflection of the design of the JVM (as opposed to an
oddity in the TJVM). The JVM provides a class argument in invokevirtual and
the argument is irrelevant to the semantics of the instruction. But the argument
is used in the implementation (via dispatch vectors) to make method resolution
faster. A nice little \metatheorem" one can prove about the TJVM is that in
a properly congured implementation lookup-method nds the same method
identied by the dispatch vector algorithm. Such a theorem was proved by Bill
Young and Rich Cohen about Cohen's dJVM.
After dening a semantic function for each TJVM instruction, we dene:

vars

(defun do-inst (inst s)
(case (op-code inst)
(PUSH (execute-PUSH inst s))

(POP (execute-POP inst s))

(LOAD (execute-LOAD inst s))

(STORE (execute-STORE inst s))

(ADD (execute-ADD inst s))

(SUB (execute-SUB inst s))

(MUL (execute-MUL inst s))

(GOTO (execute-GOTO inst s))

(IFEQ (execute-IFEQ inst s))

(IFGT (execute-IFGT inst s))

(INVOKEVIRTUAL (execute-INVOKEVIRTUAL inst s))

(INVOKESTATIC (execute-INVOKESTATIC inst s))

(RETURN (execute-RETURN inst s))

(XRETURN (execute-XRETURN inst s))

(NEW (execute-NEW inst s))

(GETFIELD (execute-GETFIELD inst s))

(PUTFIELD (execute-PUTFIELD inst s))

(HALT s)

(otherwise s)))

so that (do-inst inst s ) returns the state obtained by executing inst in state

s . The denition enumerates the instructions supported on the TJVM and calls

the appropriate semantic function.
Each of the supported instructions is modeled after one or more JVM instruc-
tions. TJVM instructions are generally simpler than their JVM counterparts. For
example, we are not concerned with access attributes, types, resource limitations,
or exceptions on the TJVM. The TJVM classes provide for \instance elds" but
do not provide the JVM's \static elds." Unlike their counterparts on the JVM,