Information Technology Reference
In-Depth Information
\21" is obtained by adding up the clocks for each instruction above.
Of interest is
(deref (top (stack (top-frame
s'
1
))) (heap
s'
1
))
. This
expression dereferences the topmost item on the operand stack of
s'
1
,withre-
spect to the heap of that state. The topmost item on the stack is, of course, the
reference that is the value of the local
p
. That reference was created by
new
at
the beginning of the program. Dereferencing it through the nal heap produces
the \logical meaning" of
p
at the conclusion of the program. The result is
(("ColoredPoint" ("color" . "Green"))
("Point" ("x" . -23) ("y" . 0))
("Object"))
This is an
instance
in the ACL2 semantics of the TJVM. It represents an object
of class
"ColoredPoint"
. It enumerates the elds of that class and of all its
superclasses and species the value of each eld. We see that at the conclusion
of the program above the
"color"
of the object is set to
"Green"
,the
"x"
eld
(in the
"Point"
superclass) is set to -23 as a result of our
"xIncrement"
and
the
"y"
eld is set to (the \uninitialized" value) 0. The
"Object"
class in the
TJVM has no elds.
5
Proving Theorems About Objects
Our
"Point"
class contains a second method, called
"inBox"
, which determines
whether its
this
object is within a given rectangle in the plane. The rectangle
is specied by two points,
p1
and
p2
, which are the lower-left and upper-right
corners of the box. Here is the denition of the method.
inBox
:
("inBox" (p1 p2)
(load p1)
;
0
(getfield "Point" "x")
;
1
(load this)
;
2
(getfield "Point" "x")
;
3
(sub)
;
4
(ifgt 21)
;
5
(load this)
;
6
(getfield "Point" "x")
;
7
(load p2)
;
8
(getfield "Point" "x")
;
9
(sub)
; 10
(ifgt 15)
; 11
(load p1)
; 12
(getfield "Point" "y")
; 13
(load this)
; 14
(getfield "Point" "y")
; 15
(sub)
; 16
(ifgt 9)
; 17
(load this)
; 18
Search WWH ::
Custom Search