topical media & game development
object-oriented programming
Specifying behavioral compositions
\label{
Cooperation}
The notion of
behavioral types
may be regarded as the formal underpinning of
the notion of
contracts specifying
the interaction between a client and server (object);
cf.
[Meyer93].
Due to the limited power of the (boolean)
assertion language, contracts as supported by
Eiffel are more limited in what may be specified
than (a general notion of) behavioral types.
However,
some of the limitations are due,
not to limitations on the assertion language,
but to the local nature of specifying object behavior by
means of contracts.
See also
[Meyer93].
To conclude this chapter,
we will look at an example illustrating the need
to specify global invariants.
Further we will briefly look at alternative formalisms
for specifying the behavior of collections of objects,
and in particular we will
explore the interpretation of
contracts as
behavioral compositions.
Global invariants
Invariants specify the constraints on the state
of a system that must be met for the system
to be consistent.
Clearly, as elementary logic teaches us,
an inconsistent system is totally unreliable.
Some inconsistencies cannot be detected locally,
within the scope of an object,
since they may be caused by actions that do not involve
the object directly.
An example of a situation in which an
externally caused inconsistent object state may occur
is given in slide
[10-invariants].
(The example is taken from
[Meyer93], but rephrased in C++.)
Problem -- dynamic aliasing
class A {
public:
A() { forward = 0; }
attach(B* b) { forward = b; b->attach(this); }
bool invariant() {
return !forward || forward->backward == this;
}
private:
B* forward;
};
class B {
public:
B() { backward = 0; }
attach(A* a) { backward = a; }
bool invariant() {
return !backward || backward->forward == this;
}
private:
A* backward;
};
slide: Establishing global invariants
When creating an instance of A, the forward pointer
to an instance of B is still empty.
Hence, after creation, the invariant of
the object is satisfied.
Similarly when, after creating an instance of B,
this instance is attached to the forward pointer,
and as a consequence the object itself is attached to the
backward pointer of the instance of B.
After this, the
invariant is still satisfied.
However, when a second instance of A is created,
for which the same instance of B is attached
to the forward pointer,
the invariant for this object will hold,
but as a result the invariance for the first
instance of A will become violated. See below.
A a1, a2; B b;
a1.attach(b);
a2.attach(b); // violates invariant a1
This violation cannot be detected by the object
itself, since it is not involved
in any activity.
Of course, it is possible to check externally
for the objects not directly involved
whether their invariants are still satisfied.
However, the cost of exhaustive checking will
in general be prohibitive.
Selective checking is feasible only
when guided by an adequate specification
of the possible interferences between object states.
Specifying interaction
Elementary logic and set-theory provide
a powerful vehicle for specifying
the behavior of a system,
including the interaction between its components.
However, taking into account that many
software developers prefer a more
operational mode of thinking
when dealing with the intricacies of
complex interactions, we will briefly look
at formalisms that allow a more explicit
specification of the operational aspects
of interaction and communication,
yet support to some extent to reason about
such specifications.
See slide [10-interaction].
Contracts -- behavioral compositions
interaction
- specification, refinement, conformance declarations
Scripts -- cooperation by enrollment
- roles, initialization/termination protocols, critical role set
Multiparty interactions -- communication primitive
- frozen state, fault-tolerance, weakening synchrony
Joint action systems -- action-oriented
- state charts, refinement, superposition
slide: Specifying interactions
In [HHG90], a notion of behavioral contracts
is introduced that allows for characterizing
the behavior of compositions of objects.
Behavioral contracts fit quite naturally in the
object oriented paradigm, since they allow
both refinement and (type) conformance declarations.
See below.
Somewhat unclear, yet, is what specification
language the behavioral contracts formalism
is intended to support.
On the other hand, from an implementation perspective
the interactions captured by behavioral contracts
seem to be expressible also within the confines
of a class system supporting generic classes
and inheritance.
A similar criticism seems to be applicable to the formalism
of (role) scripts as proposed in [Francez].
Role scripts allow the developer to specify
the behavior of a system as a set of roles and the
interaction between objects as subscribing to a role.
In contrast to behavioral contracts, the
script formalism may also be applied to describe
the behavior of concurrently active objects.
In particular, the script formalism allows
for the specification of predefined initialization and
termination policies and for the designation of
a so-called critical role set,
specifying the number and kind of participants
minimally required for a successful computation.
Also directed towards the specification of concurrent
systems is the multi-party interactions formalism
proposed in [Evangelist],
which is centered around a (synchronous) communication
primitive allowing multiple objects to interact
simultaneously.
The notion of frozen state (which may be understood as
an invariance requirement that holds during the interaction)
may be useful in particular for the specification of
fault-tolerant systems.
An interesting research issue in this respect is to what extent
the assumption of synchrony may be weakened
in favor of efficiency.
A rather different orientation towards specifying
the interaction between collections of concurrently active
objects is embodied by the joint action systems
approach described in [Kurki].
Instead of relying on the direct communication
between objects, joint action systems proceed
from the assumption that there exists some global
decision procedure that decides which actions
(and interactions) are appropriate.
Joint action systems
action by client c; server s is
when c.requesting && s.free do
<body>
slide: Specifying actions -- example
An example of an action specification is
given in slide [10-action].
Whether the service is performed depends
upon the state of both the client and the server object
selected by the action manager.
[Kurki] characterize their approach as
action-oriented to stress the importance
of specifying actions in an independent manner
(as entities separate from classes and objects).
An interesting feature of the joint action systems
approach is that the behavior of individual objects
is specified by means of state charts,
a visual specification formalism based on [Harel87].
The specification formalism adopted gives rise
to interesting variants on the object-oriented
repertoire,
such as inheritance and refinement by superposition.
From a pragmatic viewpoint, the assumption of
a global manager seems to impose high demands
on system resources.
Yet, as a specification technique, the concept
of actions may turn out to be surprisingly
powerful.
In summary, this brief survey of specification formalisms
demonstrates that there is a wide variety
of potentially useful constructs that all bear
some relevance to object-oriented modeling,
and as such may enrich the repertoire
of (object-oriented) system developers.
Contracts as protocols of interaction
Contracts as supported by Eiffel and
Annotated C++ are a very powerful means of
characterizing the interaction between a server object
and a client object.
However, with software becoming increasingly complex,
what we need is a mechanism to characterize
the behavior of collections or compositions of objects
as embodied in the notion of behavioral contracts
as introduced in [HHG90].
A contract (in the extended sense)
lists the objects that participate in the task
and characterizes the dependencies and constraints
imposed on their mutual interaction.
For example, the contract model-view, shown below
(in a slightly different notation than the original
presentation in [HHG90]), introduces
the object model and a collection of view objects.
Also, it characterizes the minimal assumptions with respect
to the functionality these objects must support
and it gives an abstract characterization of
the effect of each of the supported operations.
contract model-view< V > { MV(C)
subject : model supports [
state : V;
value( val : V ) $|->$ [state = val]; notify();
notify() $|->$ $\forall v \e $views $\bl$ v.update();
attach( v : view ) $|->$ v $\e$ views;
detach( v : view ) $|->$ v $\not\e$ views;
]
views : set where view supports [
update() $|->$ [view reflects state];
subject( m : model ) $|->$ subject = m;
]
invariant:
$\forall$ v $\e$ views $\bl$ [v reflects subject.state]
instantiation:
$\forall$ v $\e$ views $\bl$ subject.attach(v) & v.subject(subject);
subject.notify();
}
slide: The Model-View contract
To indicate the type of variables, the notation
$v : type$ is used expressing that variable v
is typed as type.
The object subject of type model has an
instance variable state of type V that
represents (in an abstract fashion) the value
of the model object.
Methods are defined using the notation
Actions may consist either of other method calls
or conditions that are considered to be satisfied
after calling the method.
Quantification as for example in
- $\A$ v $\e$ views $\bl$ v.update()
is used to express that the method $update()$
is to be called for all elements in views.
The model-view contract specifies
in more formal terms the MV part of the MVC paradigm
discussed in section [MVC].
Recall, that the idea of a model-view pair
is to distinguish between the actual
information (which is contained in the model object)
and the presentation of that information, which is
taken care of by possibly multiple view objects.
The actual protocol of interaction between a model
and its view objects is quite straightforward.
Each view object may be considered as a handler
that must minimally have a method to install
a model and a method update which is invoked,
as the result of the model object calling notify,
whenever the information contained in the model
changes.
The effect of calling $notify()$ is abstractly
characterized as a universal quantification
over the collection of view object.
Calling $notify()$ for subject results in calling
$update()$ for each view.
The meaning of $update()$ is abstractly represented as
- update() $|->$ [view reflects state];
which tells us that the state of the subject
is adequately reflected by the view object.
The invariant clause of the model-view
contract states that every change of the (state of the)
model will be reflected by each view.
The instantiation clause describes, in a rather operational way,
how to initialize each object participating in the contract.
In order to instantiate such a contract, we need to define
appropriate classes realizing the abstract entities
participating in the contract,
and further we need to define how these
classes are related to their abstract counterparts
in the contract by means of what we may call, following [HHG90],
conformance declarations.
Conformance declarations specify, in other words, how
concrete classes embody an abstract role,
in the same sense as in
in the realization of a partial type
by means of inheritance.
(C) Æliens
04/09/2009
You may not copy or print any of this material without explicit permission of the author or the publisher.
In case of other copyright issues, contact the author.
