A Formal Reference for SCOOP - Empirical Software Engineering and Verification - page 104

4.3 Heap ADT
The heap keeps track of the objects and the references associated to them. It also keeps
track of the status of once routines. This section first defines an ADT for objects and
references. Then it introduces an ADT for the heap.
Objects and references. There are two kinds of class types in the SCOOP type sys-
tem: reference class types and expanded class types. The main difference lies in the
semantics of using an instance of the types as the source of an attachment, such as as-
signment or argument passing. If an object of reference class type is the source of an
attachment, then the reference to the object gets copied over to the destination of the
attachment. The object is then accessible both through the source of the attachment as
well as through the destination of the attachment. If an object of expanded class type is
the source of an attachment, then a copy of the object gets attached to the destination of
the attachment. The details can be found in Sec. 7.4 of the Eiffel ECMA standard [9].
This formalization takes a unified view on objects and references that is compatible
with the semantics described in the Eiffel ECMA standard. It does not consider objects
of expanded class type as sub-objects in other objects or in an environment. Instead it
locates expanded objects on the heap, just like objects of reference class type. For each
object there is exactly one reference. Assigning references to objects of expanded type
has one major advantage for the formalization. If an ADT instance x that models an
object gets updated, then one gets a new ADT instance y . If one would model expanded
objects as sub-objects stored in other objects or in environments, then such an update
might trigger a cascade of ADT instance updates: each ADT instance that has x as
a query value would have to be updated with y , and so on. A consequent usage of
references avoids this issue. To do the update, one simply alters the reference to x so
that it points to y from now on.
The ADT REF models references with an identity query id and a constructor make .
The constructor uses the query new id to create a fresh identifier for the newly created
reference. The void reference void is an instance of this ADT.
The ADT OBJ models objects. Each object has a query id for its identifier, a query
class type for its class type, and a query att val for its attribute values. An object can
only have attribute values for attributes that are defined in its class type.
The attribute values of an object can be modified with the command set att val .
Only the attribute values for attributes that are defined in the class type can be modified.
The result is an updated object where the attribute value of f is set to v . Note that the
value can either be a reference or a processor. Processor values are necessary to support
processor attributes.
set att val : OBJ → FEATURE REF ∪ PROC → OBJ
o . set att val ( f , v ) require
o . class type . attributes . has ( f )
axioms
o . set att val ( f , v ) . att val ( f )= v
The constructor make can be used to create a new object. It creates a new object with
the given class type. The new object has a new identifier that is given by the query
new id . The constructor initializes all the attribute values of the new object with the
void reference.