Theoretical foundations


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