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

CLASS_TYPE FEATURE EXPRESSION

+name : NAME
+is_ref : BOOLEAN
+is_exp : BOOLEAN
+attributes : TUPLE
+functions : TUPLE
+procedures : TUPLE
+inv_exists : BOOLEAN
+inv : EXPRESSION

+name : NAME
+formals : TUPLE
+is_once : BOOLEAN
+pre_exists : BOOLEAN
+pre : EXPRESSION
+post_exists : BOOLEAN
+post : EXPRESSION
+locals : TUPLE
+body : TUPLE
+is_exported : BOOLEAN
+class_type : CLASS_TYPE

ENTITY LITERAL QUERY_CALL

+name : NAME
+context_feature : FEATURE

+obj : OBJECT

+feature_by_name(in name : NAME) : FEATURE

INSTRUCTION

ROUTINE

ASSIGNMENT COMMAND_CALL CREATION_INSTRUCTION

FUNCTION PROCEDURE ATTRIBUTE

IF_INSTRUCTION LOOP_INSTRUCTION

Fig. 1. ADTs for the intermediate representation

returns the result. This computation must not modify the state. A procedure performs a
computation that modifies the state. Functions and procedures are also known as rou-
tines. For each of these categories, CLASS TYPE defines a query that returns a tuple
of features. The query attributes returns a tuple of attributes, the query functions returns
a tuple of functions, and the query procedures returns a tuple of procedures. If the name
of a feature is known, then the query feature by name can be used to get the feature
with that name. Each class type can have an invariant. The query inv exists indicates
whether such an invariant exists. In case an invariant exists, it can be accessed with the
query inv as an expression. One of the instances of CLASS TYPE is BOOLEAN .This
class type is expanded and it has an attribute with name item . The value of this attribute
is the represented boolean value, i.e., an instance of BOOLEAN .
In this formalization, a feature is an instance of FEATURE . The name of the feature
can be retrieved with the query name and the formal arguments are given by the query
formals that returns a tuple with the formal arguments as entities. Whether or not the
feature is a once feature can be determined using the query is once . The queries pre and
post return an expression for the precondition respectively the postcondition, provided
that the queries pre exists and post exists indicate that the assertions exist. Next, there
is the query locals that gives the locals of the feature as entities. The query body returns
the body of the feature as a tuple of instructions. Each feature is either exported or not.
A non-exported feature is only available in calls on the current object within the class
that declared the feature. An exported feature can be called by other clients as well. The
query exported returns whether a feature is exported or not. Lastly, each feature has a
link to the class it belongs to. This is given by the query class type . This can be used for
example to retrieve the invariant that must be preserved by a feature. For each feature
category, there is an ADT that inherits from the FEATURE ADT.
Expressions can either be entities, literals, or query calls. Every expression is an in-
stance of EXPRESSION . For each form of expression, there is one ADT that inherits
from the EXPRESSION ADT. For entities there is an ADT with a query name that