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

The class extends "Point" (and thus "Object" ) and provides the new eld
"color" and two methods. The rst is called "setColor" and is dened below.
It sets the "color" of a "ColoredPoint" . The clock for this method returns 5.
setColor :
("setColor" (c)
(load this)
(load c)
(putfield "ColoredPoint" "color")
(return))
Consider the TJVM state
s 1 :
(make-state
(push
(make-frame 0
'((p . nil))
nil
'((new "ColoredPoint")
(store p)
(load p)
(push -23)
(invokevirtual "ColoredPoint" "xIncrement" 1)
(load p)
(push "Green")
(invokevirtual "ColoredPoint" "setColor" 1)
(load p)
(halt)))
nil)
nil
'( Point-class
ColoredPoint-class ))
This state is poised to execute the ten instruction program above, with one local,
p , which is initially nil . The class table of the state contains both "Point" and
its extension "ColoredPoint" . Inspection of the code above shows that it creates
anew "ColoredPoint" and stores it into p .Ittheninvokes "xIncrement" to
increment the "x" eld of p by -23 and invokes "setColor" to set the "color"
eld of p to "Green" . Of interest is the fact that the rst method is in the class
"Point" and the second is in the class "ColoredPoint" .The "ColoredPoint"
p inherits the elds and methods of its superclass, "Point" .
Had the "ColoredPoint" class overridden the method "xIncrement" by in-
cluding the denition of such a method, then the program above would have in-
voked that method rather than the one in "Point" , since the method is selected
by searching through the superclass chain of the this object of the invocation,
which is here p , an object of class "ColoredPoint" .
Consider, s' 1 , the result of running the TJVM on s 1 for21steps,
s' 1 :
(tjvm s 1 21).