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

arise with "Point" instances because their elds do not contain references. But
consider the class "LinkedList" , with two elds, "head" and "next" . Suppose
the "next" eld generally contains a (reference to a) "LinkedList" instance.
Then a typical instance of "LinkedList" might be:

(("LinkedList" ("head" . 1) ("next" . (REF 45)))
("Object")).

Since the object itself might be \circular" we cannot, in general, replace (REF
45) by the instance to which it dereferences. Thus, we see that while instances
may be more convenient than references for simple classes like "Point" ,they
are no more convenient than references in general.
We therefore chose references because it tends to induce a uniform style in
the denition of the logical functions for manipulating objects, that style being
to dereference the reference with respect to the state, use the resulting instance
and then recursively deal with the interior references. This means that the Lisp
formalization of the semantics of a TJVM method may very closely resemble
the algorithm implemented by the byte code. This is convenient because the
verication of a method generally takes place in two steps. In the rst step we
prove that the interpretation of the byte code produces the same TJVM state
transformation as described at a higher level by the Lisp function. In the second
step we prove that the Lisp function enjoys some desirable properties. The rst
step is complicated by the semantics of the byte code interpreter and so it is
convenient for the Lisp to be \close" to the byte code. Once we have gotten
away from the byte code to the simpler applicative Lisp world, we deal with the
complexity of proving that the Lisp \does the right thing."
In this paper we do not further consider instances that reference other in-
stances.
We next consider the "inBox" method and focus on its \clock function."
How many TJVM cycles are required to execute an invocation of that method?
We can express the clock function for "inBox" with:

(defun inBox-clock ( this p 1 p 2 s )
(cond ((> (Point.x p 1 s )
(Point.x this s ))

9)
((> (Point.x this s )
(Point.x p 2 s ))

15)
((> (Point.y p 1 s )
(Point.y this s ))

21)
(t 27)))

Despite the apparent simplicity of the "inBox" method, the time it takes depends
not only on the inputs p 2 , but on the state in which it is called.

This is unavoidable since the very meaning of references to objects change as
the heap changes.

this , p 1 ,and