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

The processor separator | is commutative and associative, i.e., p 1 :: s 1 | p 2 :: s 2 = p 2 ::

s 2 p 3 :: s 3 . Within an

action queue, ; separates statements. The configuration is well-defined if and only if
¬∃

| p 1 :: s 1 and p 1 :: s 1 | ( p 2 :: s 2 | p 3 :: s 3 )=( p 1 :: s 1 | p 2 :: s 2 ) |

i , j ∈{ 1 ,..., n } : p i = p j .

Statements. A statement is an element of the action queue. A statement is either an
instruction or an operation. An instruction is user syntax, i.e. an action that occurs
explicitly in the SCOOP program. An operation is run-time syntax, i.e. an action that
does not explicitly occur in a SCOOP program. For example, locking of request queues
is not an action that is explicit in a SCOOP program. Instead, locking is based on the
formal argument list. It is done implicitly before a feature gets executed.

Transitions. A transition takes a system in a start configuration and leaves it in a
result configuration. The following shows the general form of a transition definition
that declares a start configuration with schedule P de f

P , σ = p 1 :: s 1 | ... | p n :: s n and a

de f
= P , σ with schedule P p 1 :: s 1 p m :: s m : result configuration | ... |

Γ P , σ → P , σ

The typing environment can be used in the transition definition to access static infor-

mation about the SCOOP program.

Γ

Inference rules. An inference rule describes the circumstances under which a transi-
tion can be used. The inference rule has a premise and a conclusion. The conclusion is
the transition and the premise describes the circumstances under which the transition
can be used. The premise consists of a number of transitions and a side condition. The
premise is satisfied if all transitions in the premise can be taken and if the side condition
is true. In this formalization, most of the rules have no transition in the premise. The
following simplified inference rule template takes this into account:

Simplified Inference Rule Template
condition
new state σ definition
fresh channels definitions
Γ P , σ → P , σ

The side condition has three parts. The first part defines a condition that is based on
the typing environment and the start configuration. The second part is the new state
definition that defines the state of the result configuration. This new state is based on the
state in the start configuration. The last part consists of the fresh channels definitions .
Auxiliary definitions can be used in the condition, the new state definition, and the
fresh channels definitions. The side condition can mention features of STATE .The
preconditions of these features serve as additional conditions in the side condition.
The following inference rule generalizes transitions by adding processors both to the
start configuration and to the result configuration. These additional processors run in
parallel but do not take any actions during the generalized transition.