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

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

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

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

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

setColorBox ))

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

This theorem is exactly analogous to the one about "inBox" . The eect of the
theorem is to congure ACL2 so that when it sees a tjvm expression with the
setColorBox-clock it increments the program counter by one, pops four things
o the operand stack, and sets the heap to that described by setColorBox-heap .
Such a move is interesting by virtue of the following easy-to-prove theorem
about that heap:

Theorem.
(implies (and (refp ref )
(refp this ))
(equal (deref ref
(setColorBox-heap this p 1 p 2 color s ))
(if (and (equal ref this )
(inBox this p 1 p 2 s ))
(set-instance-field "ColoredPoint" "color" color
(deref this (heap s )))
(deref ref (heap s )))))

This theorem species the key property of the new heap. It denes how to
dereference an arbitrary reference, ref , with respect to the new heap. If ref is