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

push env with feature : STATE → PROC FEATURE → REF → TUPLE STATE
σ . push env with feature ( p , f , r 0 , ( r 1 ,..., r n )) require
σ . regions . procs . has ( p )
f . formals . count = n
∀ i ∈{ 0 ,..., n } : r i = void → σ . heap . refs . has ( r i )

axioms
σ . push env with feature ( p , f , r 0 , ( r 1 ,..., r n )) =
σ n . set ( σ n . regions , σ n . heap , σ n . store . push env ( p , e ))
where
σ 0 de f = σ

∀ i ∈{ 1 ,..., n } : ( σ i , r i )

de f
=

⎨
⎩

= void ∧ σ i − 1 . handler ( r i ) = p if ∃ d , q , c : Γ f . formals ( i ) : ( d , q , c ) ∧ c . is exp ∧ r i

( σ x , σ x . last imported ref )
where
σ x de f

= σ i − 1 . deep import ( p , r i )
if ∃ d , q , c : = void ∧ σ i − 1 . handler ( r i )= p Γ f . formals ( i ) : ( d , q , c ) ∧ c . is exp ∧ r i

( σ x , σ x . last added obj )
where
σ x de f

= σ i − 1 . add obj ( p , σ i − 1 . heap . ref obj ( r i ) . copy )
otherwise
( σ i − 1 , r i )

w de f = new ENV . make

. update ( f . formals ( 1 ) . name , r 1 ) ... . update ( f . formals ( n ) . name , r n )
. update ( f . locals ( 1 ) . name , void ) ... . update ( f . locals ( f . locals . count ) . name , void )
. update ( Current , r 0 )
e de f

w if f ∈ PROCEDURE
w . update ( Result , void ) if f ∈ FUNCTION

=

In a first step, the auxiliary command defines an updated state, in which p gets a new
initialized environment e . The updated state is based on an intermediate state σ n ,which

gets defined in a cascade of state updates with the goal of either copying or deep im-
porting the actual arguments of expanded type. The cascade starts with the definition of
a starting state

σ 0 . For each formal argument, the cascade defines a tuple ( σ i , r i ) with an

updated state and a reference. If the corresponding actual argument is of reference class
type, nothing needs to be done. If the actual argument is of expanded class type and the
referenced object is not handled by p ,then p must deep import the object structure. This
results in an updated state and a new reference to the deep imported object structure.
If the actual argument is of expanded class type and the referenced object is handled
by p , then the expanded object must be copied. This results in an updated state and a
new reference to the copy. The resulting state σ n contains all the deep imported and

copied objects. The resulting references r 1 ,..., r n will be used for values of the formal

argument names.
In a next step, the command defines the environment w as a new environment that
gets updated to map formal argument names, local variable names, the current entity
name, and the result entity name to the respective values. The names of the formal
arguments get mapped to the references r 1 ,...,

r n . Names of local variables are mapped
to the void reference. The current entity name is mapped to the target reference.