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

either has an unqualified or a qualified specification. An unqualified explicit processor
specification , i.e., < p > , is based on a processor attribute p . The processor attribute

and it must be declared in the same class as
the explicit processor specification or in one of the ancestors. The processor denoted
by this explicit processor specification is the processor stored in p .A qualified explicit
processor specification , i.e.,

p must have the type ( ! , •, PROCESSOR )

, relies on an entity e occurring in the same
class as the explicit processor specification or in one of the ancestors. The entity e must
be a non-writable entity of attached type and the type of e must not have a qualified
explicit processor tag. The processor denoted by this explicit processor specification is
the same processor as the one of the object referenced by e . Explicit processor tags sup-
port precise reasoning about object locality. Entities declared with the same processor
tag represent objects handled by the same processor. The absence of both the keywords
is treated as if there was an attached keyword.

< e . handler >

3.2 Simplifications

This work makes the following simplifications:

- It does not consider unqualified feature calls. It expects all feature calls to be in the
qualified form. This includes accesses to attributes of the current object in expres-
sions.
- It does not consider infix feature calls. It expects all feature calls in the non-infix
form. For example, an expression x > y must be transformed into the equivalent

form x . is greater ( y ).
- It simplifies the automatic initialization of entities. All entities, except for the cur-
rent object entity, are initialized with the void reference.
- It neglects exception handling. The exception handling mechanism for SCOOP is
still under development.
- It does not consider garbage collection because garbage collection is not refined in
the SCOOP model.
- It does not consider agents. From this work's point of view, agents are normal
objects.

3.3 Intermediate Representation

For the purpose of the formalization, this work assumes that a program is given in
an enriched intermediate representation, where the syntactical elements are replaced
with instances of abstract data types. In particular, it assumes ADTs for class types,
features, expressions, and instructions. Fig. 1 summarizes these ADTs. The instances
of CLASS TYPE are all possible class types, i.e., the types directly defined by all
non-generic classes and all possible generic derivations of all possible generic classes.
Sec. 4.1 discusses how to get these instances. The ADT CLASS TYPE defines a name
query name . Each class type can either be a reference class type or an expanded class
type. The queries is ref and is exp provide this information. Each class type defines a
number of features. These features can be divided into attributes, functions, and proce-
dures. An attribute of an object stores a value. A function performs a computation and