Information Technology Reference
In-Depth Information
make
:
CLASS TYPE
→
OBJ
axioms
make
(
c
)
.
id
=
new id
make
(
c
)
.
class type
=
c
∀
i
∈{
1
,...,
n
}
:
make
(
c
)
.
att val
(
a
i
)=
void
where
{
a
1
,...,
a
n
}
de f
=
c
.
attributes
An object can also be copied with the auxiliary query
copy
. This is important for ex-
panded objects with copy semantics. The copied object has the same class type and the
same attribute values as the original object, but it has a new identity. The new identity
comes from the call to the constructor
make
.
copy
:
OBJ
→
OBJ
axioms
o
.
copy
=
make
(
o
.
class type
)
.
set att val
(
a
1
,
o
.
att val
(
a
1
))
. ...
.
set att val
(
a
n
,
o
.
att val
(
a
n
))
where
n
de f
=
o
.
class type
.
attributes
.
count
{
a
1
,...,
a
n
}
de f
=
o
.
class type
.
attributes
Mapping from references to objects.
The ADT
HEAP
makes use of
OBJ
and
REF
to model the mapping from references to objects. For this purpose, it declares the query
objs
to store all the objects on the heap and it declares the query
refs
to get all the
references to these objects. The reference
void
is not part of the reference set. The
query
ref obj
defines the actual mapping. For each reference in
refs
an object in
objs
gets returned. The ADT also declares the query
last added obj
to keep track of the last
object that has been added to the heap. It uses this query to define the effect of adding
an object to the heap.
objs
:
HEAP
→
SET
[
OBJ
]
refs
:
HEAP
→
SET
[
REF
]
ref obj
:
HEAP
→
REF
OBJ
h
.
ref obj
(
r
)
require
h
.
refs
.
has
(
r
)
last added obj
:
HEAP
→
OBJ
h
.
last added obj
require
¬
h
.
objs
.
is empty
A number of commands are responsible for adding objects and for altering the mapping of
references to objects. The command
add obj
takes an object
o
and adds it to the heap. The
result of the command is a new heap with the object
o
and a new reference that points
Search WWH ::
Custom Search