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

"Point" "inBox" 2) we require that it be a list whose rst, third and fourth
elements are invokevirtual , "inBox" and 2, respectively.
The second change to this approximation is that we must insist that the
method found by looking up the superclass chain of

be inBox . In par-
ticular, just because we invoke "inBox" in a TJVM state in which "Point" is
dened as above, do we know that the resolved method will be inBox ? No! The
superclass chain of

this

this

might include a class that overrides "inBox" and denes
it a dierent way. If we add the hypothesis that the resolved method is inBox
then we may delete the hypothesis, in our approximation above, requiring that
"Point" be as dened here: it does not matter how "Point" is dened as long
as the resolved method is our inBox .

Theorem. "inBox" is correct: Suppose s 0 is a TJVM state whose next

instruction is of the form (invokevirtual class "inBox" 2) . Let this

be the third item on the operand stack, let p 1 be the second item, and

let p 2 be the topmost item. Suppose the nearest method named "inBox"

in the superclass chain of this is inBox . Then the TJVM state obtained

by stepping s 0 with the

program counter incremented by one and the three items removed from
the operand stack and replaced by 1 or 0 according to whether (inBox
this p 1

s 0 (inBox-clock this p 1 p 2 s 0 ) times is state

p 2 s 0 ) . The heap is unchanged.

Here is the formal rendering of the theorem:

Theorem. "inBox" is correct:
(implies (and (consp (next-inst s 0 ))
(equal (car (next-inst s 0 )) 'invokevirtual)
(equal (caddr (next-inst s 0 )) "inBox")
(equal (cadddr (next-inst s 0 )) 2)

(equal this (top (pop (pop (stack (top-frame s 0 ))))))
(equal p 1

(top (pop (stack (top-frame s 0 )))))

(equal p 2 (top (stack (top-frame s 0 ))))

(equal (lookup-method "inBox"
(class-name-of-ref this (heap s 0 ))
(class-table s 0 ))

inBox ))

(equal
(tjvm s 0 (inBox-clock this p 1 p 2 s 0 ))
(make-state
(push (make-frame (+ 1 (pc (top-frame s 0 )))
(locals (top-frame s 0 ))
(push (if (inBox this p 1 p 2 s 0 )10)
(popn 3 (stack (top-frame s 0 ))))
(program (top-frame s 0 )))
(pop (call-stack s 0 )))
(heap s 0 )
(class-table s 0 ))))