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

inBox rather than, say, fact . We can recover most of the former eciency while
preserving the wide applicability of the theorem by using the left-hand side (tjvm
s 0 (inBox-clock

this p 1 p 2 s 1 )) and adding the additional hypothesis that

this p 1 p 2 s 1 ) is equal to (inBox-clock this p 1 p 2 s 0 ) .That

(inBox-clock

is, we can give the two original occurrences of s 0 dierent names and merely

insist that inBox-clock return the same thing on both of them. This is our
preferred phrasing. We now return to the main flow of our presentation.
We nally turn to a theorem about a method that modies an object, i.e.,
that modies the heap. This is the second method of the "ColoredPoint" class:

setColorBox :
("setColorBox" (p1 p2 color)
(load this)
(load p1)
(load p2)
(invokevirtual "ColoredPoint" "inBox" 2)
(ifeq 4)
(load this)
(load color)
(putfield "ColoredPoint" "color")
(return))

This void instance method takes three arguments, two points and a color. If the
\this" object is in the box specied by the two points, the method sets the color
of the \this" object to the specied color. The clock function for "setColorBox"
is

(defun setColorBox-clock ( this p 1

p 2 cs )

(declare (ignore c ))
(++ 4
(inBox-clock this p 1 p 2 s )
(if (inBox this p 1 p 2 s )
5
2)))

The primary eect of invoking "setColorBox" is to produce a new heap. That
heap is described by

(defun setColorBox-heap ( this p 1 p 2 cs )
(if (inBox this p 1 p 2 s )
(let (( instance (deref this (heap s )))
( address (cadr this )))
(bind
address
(set-instance-field "ColoredPoint" "color" c instance )
(heap s )))
(heap s )))

The theorem stating the correctness of "setColorBox" is