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

to o . The newly added object is indicated in the query last added obj . Note that this
command does not create a new object. It simply adds an object that has been provided
as an argument. The command requires that the object is not yet part of the heap.

add obj : HEAP → OBJ HEAP
h . add obj ( o ) require
∀ u ∈ h . objs : u . id = o . id
∀ a ∈ o . class type . attributes :
o . att val ( a ) ∈ REF → ( o . att val ( a )= void ∨ h . refs . has ( o . att val ( a )))
axioms
h . add obj ( o ) . objs = h . objs ∪{ o }
h . add obj ( o ) . refs = h . refs ∪{ r }
h . add obj ( o ) . ref obj ( r )= o
h . add obj ( o ) . last added obj = o
where
r de f = new REF . make

If an object that is already part of the heap gets updated, then it is necessary to update
the mapping from the reference to the object on the heap. This can be done with the
command update ref that takes a reference r and an updated object o and returns a
heap where the reference r points to o . The command requires that r is a valid reference
and that o is an updated version of the original object. Because the remaining part of
the state only deals with references rather than objects directly, a reference update does
not require an update of these parts.

update ref : HEAP → REF OBJ HEAP
h . update ref ( r , o ) require
h . refs . has ( r )
o . id = h . ref obj ( r ) . id
∀ a ∈ o . class type . attributes :
o . att val ( a ) ∈ REF → ( o . att val ( a )= void ∨ h . refs . has ( o . att val ( a )))
axioms
h . update ref ( r , o ) . objs . has ( o )
o = h . ref obj ( r ) →¬ h . update ref ( r , o ) . objs . has ( h . ref obj ( r ))
h . update ref ( r , o ) . ref obj ( r )= o
h . last added obj = h . ref obj ( r ) → h . update ref ( r , o ) . last added obj = o

So far HEAP covers the mapping from references to objects. Occasionally it is neces-
sary to have the inverse mapping. The commands add obj and update ref ensure that
there is exactly one reference for each object on the heap. Thus it is possible to define
the inverse query ref as an auxiliary query.

ref : HEAP → OBJ REF
h . ref ( o ) require
h . objs . has ( o )
axioms
h . ref obj ( h . ref ( o )) = o

Once routines. A once routine can either be a once function or a once procedure. A
once routine gets executed at most once in a certain context. If a once routine has been
executed in the context, then it is called non-fresh in the context. Otherwise it is called