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

our INVOKEVIRTUAL and INVOKESTATIC do not take \signatures." On the JVM,
a method's \this" object is in local variable 0; on the TJVM it is an implicit
formal parameter named this . Like its JVM counterpart, the method actually
invoked by our INVOKEVIRTUAL depends on the \this" object: both invoke the
nearest method of the given name found in the superclass chain of the object,
but the JVM discriminates between candidate methods via their signatures and
we do not. That is, the JVM supports \overloading" and the TJVM does not.
The \single stepper" for the TJVM is

(defun step ( s )
(do-inst (next-inst s ) s ))

where next-inst retrieves the instruction indicated by the program counter in
the topmost frame of the call stack.
TheTJVMisthendenedasaniteratedstepfunction:

(defun tjvm ( sn )
(if (zp n )
s
(tjvm (step s )(- n 1))))

times, or (step n Thus (tjvm ) .

The TJVM can be viewed as a simplication of the JVM. The TJVM is in
fact a simplication of Rich Cohen's \defensive JVM", [6], which includes many
more JVM instructions and deals carefully with the preconditions assumed for
each instruction. In principle, Cohen's specication could be used to analyze
whether a given byte code verier is sucient to guarantee the absence of certain
classes of runtime errors. Both the TJVM and the defensive JVM omit major
aspects of the JVM, including floating point numbers, arrays, multiple threads,
exceptions, and native methods. All but native methods could be formalized in
an implementation independent way, following the basic approach.

sn ) is the result of applying step to sn s

2 Example TJVM Executions

Having dened the TJVM in Lisp, it is possible to execute it on concrete data.
Consider the byte code for the "fact" program shown earlier in the constant
Fact . Let Math-class denote the list constant partially displayed below.

Math-class :
("Math" ("Object") () ( ::: Fact ::: )).

This is a class declaration for a class called "Math" whichisanextensionofthe
class named "Object" (literally, the declaration says that the superclass chain
of "Math" is the list containing only the class named "Object" ). The "Math"
class contains no elds and its methods are those listed and include Fact .
Consider the TJVM state