Information Technology Reference
In-Depth Information
(getfield "Point" "y")
; 19
(load p2)
; 20
(getfield "Point" "y")
; 21
(sub)
; 22
(ifgt 3)
; 23
(push 1)
; 24
(xreturn)
; 25
(push 0)
; 26
(xreturn))
; 27
This is a straightforward compilation (for the TJVM) of the following Java
(which is written in a slightly awkward style to make the correspondence with
the byte code more clear).
public boolean inBox(Point p1, Point p2)
f
if (p1.x <= this.x &
this.x <= p2.x &
p1.y <= this.y &
this.y <= p2.y)
f
return true;
g
else
f
return false;
gg
We will specify and prove the correctness of this method in a moment. But
we must develop some Lisp functions for dealing with points and in so doing
illustrate our preferred style for dealing with TJVM objects in general, at the
logical level.
Consider the two Lisp functions below for retrieving the x- and y-coordinates
of a point.
(defun Point.x (
ref s
)
(field-value "Point" "x" (deref
ref
(heap
s
))))
(defun Point.y (
ref s
)
(field-value "Point" "y" (deref
ref
(heap
s
))))
Observe that they take the TJVM state,
, as arguments. That is because we
apply them to
references
to Points, not to
instances
. Had we chosen the latter
course, we would have dened
Point.x
as
s
(defun Point.x (
p
)
(field-value "Point" "x"
p
))
but would have to call it by writing
(Point.x (deref
ref
(heap
s
)))
.Webe-
labor this point for a reason: when dening the Lisp concepts necessary to speak
formally about TJVM objects should we focus on references or on instances?
If we focus on references, we must also have available the state, or at least the
heap, with respect to which those references are to be dereferenced. This is the
choice we have made and yet it seems complicated.
The problem with focusing on instances is that instances may contain refer-
ences. Thus, even if we focus on instances the heap is still relevant. This does not
Search WWH ::
Custom Search