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

If Operation - True

⎨
⎩

x if x ∈ BOOLEAN

y de f = σ . att val ( σ . ref obj ( x ) , item ) if x ∈ REF ∧ σ . ref obj ( x ) . class type = BOOLEAN

false otherwise

y = true

Γ p :: provided x then s t else s f end ; s p , σ → p :: s t ; s p , σ

If Operation - False

⎨
⎩

x if x ∈ BOOLEAN
σ . att val ( σ . ref obj ( x ) , item ) if x ∈ REF ∧ σ . ref obj ( x ) . class type = BOOLEAN
true

y de f =

otherwise

y = false

Γ p :: provided x then s t else s f end ; s p , σ → p :: s f ; s p , σ
The provided x then s t else s f end operation has two branches. Sometimes it is
necessary to only have one branch. The nop operation can be executed without an effect.
It can be used in the conditional operation to define an empty branch. The nop operation
can also be used to indicate that an action queue is empty.

No Operation

Γ p :: nop ; s p , σ → p :: s p , σ

5.4 Code Elements

This section explains the semantics of code elements: entity expressions, literal expres-
sions, feature calls, feature applications, creation instructions, flow control instructions,
and assignment instructions.

Entity expressions. A variant of the eval ( operation evaluates entity expressions.

The operation uses the read operation to send a notification with the value of the entity
over a new channel a . It then uses the value of this channel to define the result of the
eval operation.
Entity Expression

a , e )

e ∈ ENTITY
a is f resh
Γ p :: eval ( a , e ) ; s p , σ → p :: read ( e . name , a ) ; result ( a , a . data ) ; s p , σ

Literal expressions. Another variant of the eval ( operation evaluates literal ex-

pressions. To evaluate a non-void literal expression, the operation creates a new object
of the literal class type so that the new object represents the literal value. For this pur-
pose, it uses the query obj of LITERAL . Since the type of every literal is non-separate,
it creates the new object on the processor that evaluates the literal expression. The ref-
erence r to the new object is the result of the evaluation. To evaluate a void literal, the
operation takes the void reference.

a , e )