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

The identity of an ADT instance is given by its query values. Hence, the following holds
for all ADTs t : new t . constructor ( e 1 ,..., e n )= new t . constructor ( e 1 ,..., e n ) .

Example 1 (Functional notation versus object-oriented notation). The expression in
functional notation is empty

( ( ( [ ] . , )))

pop push new STACK PROC make p can be written

[ ] . . ( ) . .

in object-oriented notation as new STACK PROC make push p pop is empty .

Each feature can have a precondition that must be satisfied before the feature gets called.
A precondition is expressed as a number of assertions on the target and the arguments.
A feature with a precondition is a partial feature. A partial feature is a feature whose
domain is restricted. Such a partial feature is indicated with a crossed arrow

after
the type of each formal argument that got restricted by the feature's precondition. Non-
restricted formal arguments are indicated with a normal arrow . The effect of an ADT

command is described in a number of axioms. This work deviates from the practice of
bundling all axioms for a specific ADT. Instead, all the axioms for a specific feature
occur in the feature's declaration. Note that this work does not aspire a sufficiently
complete ADT because this would lead to rule explosion. An ADT is sufficiently com-
plete if its axioms make it possible to reduce any query expression to a form that does
not involve an instance of the ADT. This requires that the axioms describe the effect of
each command on each query. This work follows the practice to describe the effect of
each command of an ADT on all the queries of the ADT that have been changed by the
command. Unmentioned queries are unchanged.

→

Example 2 (Command declaration). The following declaration shows a command to
set the value of an attribute f of an object o to the value v . The value can either be
a reference or a processor. The command takes the object as the target and returns an
updated object whose attribute value is set.

set att val : OBJ → FEATURE REF ∪ PROC → OBJ
o . set att val ( f , v ) require
o . class type . attributes . has ( f )
axioms
o . set att val ( f , v ) . att val ( f )= v

The command states in its precondition that the class type of the target object o must
have an attribute f . This is expressed as an assertion after the require keyword. The part
in front of the require keyword gives names to the target and the arguments. Note that
the precondition makes the command partial. The updated object has the value of its
attribute f set to v . This is stated as an axiom after the ensure keyword.

So far the discussion covered queries, commands, and constructors for ADTs. This work
extends the ADT theory with the notion of auxiliary features. Auxiliary features are
convenience features that are not essential for the definition of the ADT, but nevertheless
useful.
The remainder of this work declares various ADTs to model the state of a SCOOP
program. Unless it would create confusion, it uses the same name for an instance of
an ADT and the corresponding domain element. For example, the instance of the ADT
OBJ is called an object.