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

The environment w is the final environment e in which the result name gets mapped
to the void reference. This environment and the updated state σ n define the result of the

command. The auxiliary command push env pushes e onto p 's stack of environments.
The auxiliary command push env takes a processor p and an environment e . It returns
a state in which e is pushed on top of p 's environment stack.
The effect of a call to push env with feature or a call to push env can be undone with
a call to the auxiliary command pop env . This auxiliary command takes a processor p
and removes the top environment from p 's stack of environments.

Setting values of local variables and the value of the result entity. The values of local
variables and the value of the result entity are maintained in the store. The auxiliary
command set env val sets a value v for the name n in processor p 's top environment.
For this, it defines an updated environment e in which n is set to v . It then defines
an updated store s by first removing the top environment and then adding the updated
environment e . The updated store is then used to define an updated state. The updated
state becomes the result of the auxiliary command.

Setting attribute values of the current object. The auxiliary command set att val takes
an object o ,aname n , and a value v . It returns an updated state in which the attribute
with name n of object o is set to the value v . In a first step, the auxiliary command
defines an updated object with a call to set att val . This updated object is then used to
update the existing reference to o in the state.

Setting values of local variables, the value of the result entity, and attribute values of
the current object in a unified way. The auxiliary command set val attaches a value v
to an entity with name n . The entity can either be a local variable or the result entity in
the top environment of p . It can also be an attribute of the current object on p . In either
case, the update affects an entity on p .
The definition of the resulting state is based on the auxiliary definitions o , σ ,and

v . The definition o defines the current object, as defined by the top environment of
processor p . The precondition makes sure that there is always such an environment on
p where the current object is defined. If v is a reference and the referenced object is an
object of reference class type, then v can be attached directly to the entity with name n .
If the object is an expanded object handled by processor p , then the referenced object
must first be copied. Expanded objects handled by a processor different than p must be
deep imported. However, this is done right when the object gets returned from another
processor to p . The definitions

σ and v

define a state and a value that are potentially

updated according to these rules.
The state σ must be updated with the value v . The update can either affect the

current object on p or it can affect the top environment of p . Attribute names of the
current object, local variable names, and formal argument names are distinct. Therefore
it is safe to first check whether the current object o has an attribute with name n ,in
which case the current object gets updated with a v . If the current object does not have
such an attribute, then it is safe to assume that the top environment contains an entity
with name n , in which case the top environment gets updated.