introduction
teaching
contracts
patterns
events
examples
foundations
conclusions
references
The relevance of the notions presented can be clearly
motivated from the practice of the software engineering
of OO systems.
For the (academic) student of OO it is interesting to note
that there is a substantial amount of theory
related to the notion of contracts and that research
aimed at developing suitable formalisms for
characterizing the behavior of complex object systems
is well on its way.
A behavioral interpretation of types
From a theoretical perspective a type denotes essentially
a set of elements.
Sybtyping is, technically, a means of narrowing
the set of elements belonging to a type
by providing additional information concerning the (sub) type.
The principal subtyping requirement may be expressed
as a 'substitutability rule', which says that
(when B is a subtype of A) any element of (subtype) B
may be used where an element of (type) A is expected.
This requirement results in subtyping rules for
enumeration types, function types and record types,
that respect resp. subset containment, contra-variance of
argument types and record (subtype) extensions
[Cardelli].
These subtyping rules, however, still have a syntactic flavor.
One step further is to think of types as representing
entities of which the behavior
is characterized by means of prediactes or logical formulas
[Wegner].
The notion of contracts is closely related to
a behavioral interpretation of types.
Usually, students are already well-versed
in employing 'abstract data types'
and their (mathematical) interpretation
as entities that are characterized primarily
by the operations they may be subjected to.
From there, it is a small step to think of
classes as types of which the behavioral
aspects are specified in terms of
object state invariants and method pre- and post-conditions.
In particular there is a close correspondence
between the guidelines resulting from
the (supplier/client) metaphor underlying
contracts in actual software development
and the substitutibiliy requirement
as employed in a theoretical characterization
of subtyping.
The substitutability requirement states
that any element of a subtype can be used
wherever an element of the (super) type is expected.
This requirement is clearly satisfied for an object
instance of a subclass when its associated contract
satisfies the contract refinement relation,
namely pre-conditions can only be relaxed
and it's result or method's post-conditions
will be more narrowly specified.
A more thorough treatment of these notions can be found
in [America,Liskov].
This material provides also the foundations for
the verification of object systems using an extension to
Hoare logic [deBoer].
Complex interactions between objects
There is no (such) consensus on what would be a suitable
formalism for expressing the interaction between a collection
of objects.
Yet, there is a growing body of literature dealing with
object interaction and multi-party communication
[Multiparty,Script].
Promising seems the notion of behavioral contracts
as presented in [Helm].
A behavioral contract lists the objects that
participate in the tasks and characterizes the
dependencies and constraints imposed on their
mutual interactions.
In order to instantiate such a contract (in the extended sense),
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 by means
of so-called conformance declarations.
introduction
teaching
contracts
patterns
events
examples
foundations
conclusions
references