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

Identifier management. This formalization models objects, references, and proces-
sors. All of these domain elements have an identity. These identities are automatically
managed by the runtime system. The work by Khoshafian and Copeland [16] on differ-
ent levels of object identity provides good reasons for this decision. They introduce a
scale that starts with identities given by the value, goes on with user-supplied identities,
and ends with built-in identities. Built-in identities have the advantage that the iden-
tities are preserved in case of modifications. According to this hierarchy, our domain
elements have a built-in identity. One straightforward way to reflect this, is to model
each domain element as an instance of an ADT. However, this direct approach does not
properly capture the identities of the domain elements because the identity of an ADT
instance is not built-in, but based on the query values. This section describes a way to
introduce built-in identities for ADT instances.
To model domain elements with built-in identities, one can define an ADT with an
identifier query. A number of ADT instances represent a single domain element over
time. Each of the ADT instances has the same value for the identifier query. A modi-
fication of the domain element can then be modeled as a new ADT instance where the
value of the identity query is preserved and all other queries modulo the modification
are preserved.
For this to work, the formalization ensures that no two ADT instances that model
different domain elements have the same identity. This is ensured with a fresh identifier
for each ADT instance that models a new domain element. For this purpose, the univer-
sal stateful query new id returns a fresh identifier. The formalization then preserves the
identifier in every modification.

Typing environment. Nienaltowski [25] presents a formalization of the SCOOP type
system for a core of SCOOP called SCOOP C . The type system formalization is part
of the base for this work. The typing environment contains the class hierarchy of a

SCOOP program along with all the type definitions of all features and entities. Type
rules allow us to derive conclusions.
The notation

Γ

Γ e : t denotes that expression e is of type t . Based on this derivation,

the function type of ( Γ , e ) denotes the type of expression e in the typing environment

Γ . The type rules can be used to check whether an expression is controlled or not. In a

SCOOP program, each processor p that wants to apply a feature f must make sure that
all the processors of all attached actual arguments of f are exclusively avail-

able on behalf of processor p . This guarantees exclusive access on all objects handled
by processors

( q 1 ,..., q n )

. Note that processor p is in this set too because p can ex-
clusively access its objects during a feature execution. For safety, the type system only
allows feature calls in f on expressions, where the type system can derive that the value
of the expression is a reference to an object and this object is handled by one of the
processors

{ p , q 1 ,..., q n }

. Such an expression is called controlled . Whether or not an
expression is controlled can be determined through the context in which the expression
appears and the type of the expression. The context can either be the enclosing class, in
case of expressions in invariants, or it can be the enclosing feature, in case of all other
expressions. To be more precise, an expression e of type t

{ p , q 1 ,..., q n }

=( d , p , c ) is controlled if and

only if t is attached, i.e., d = !, and t satisfies at least one of the following conditions: