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

Environments. The ADT ENV has a query names that stores all the defined names.
The query val can then be used to get the value for each such name.

names : ENV → SET [ NAME ]

val : ENV → NAME REF ∪ PROC
e . val ( n ) require
e . names . has ( n )
The command update takes a name and a value and returns an updated environment.
Note that it does not matter whether the name is already defined in the environment or
not. In any case, the name will be defined in the updated environment and the name will
be mapped to the value. The value can either be a reference or a processor. Environments
with processor values are not strictly needed to describe SCOOP, however they make it
possible to have a unified view on attribute values and environment values.

update : ENV → NAME → REF ∪ PROC → ENV
axioms
e . update ( n , v ) . names = e . names ∪{ n }
e . update ( n , v ) . val ( n )= v
The constructor make returns an empty environment.

make : ENV
axioms
make . names . is empty

Mapping from processors to environments. The ADT STORE has a single query
envs that stores a stack of environments for each processor.

envs : STORE → PROC → STACK [ ENV ]

The command push env pushes a given environment on top a processor's stack of envi-
ronments. The command pop env pops the top environment from a non-empty stack of
environments.

push env : STORE → PROC → ENV → STORE
axioms
s . push env ( p , e ) . envs ( p )= s . envs ( p ) . push ( e )

pop env : STORE → PROC STORE
s . pop env ( p ) require
¬ s . envs ( p ) . is empty
axioms
s . pop env ( p ) . envs ( p )= s . envs ( p ) . pop
The constructor make creates an empty store.

make : STORE
axioms
∀ p ∈ PROC : make . envs ( p ) . is empty