topical media & game development

talk show tell print

object-oriented programming

From specification to implementation


Designing an object-oriented system requires the identification of object classes and the characterization of their responsibilities, preferably by means of contracts.

In addition, one must establish the relationships between the object classes constituting the system and delineate the facilities the system offers to the user. Such facilities are usually derived from a requirements document and may be formally specified in terms of abstract operations on the system.

In this section we will look at the means we have available to express the properties of our object model, and we will study how we may employ abstract specifications of system operations to arrive at the integration of user actions and the object model underlying a system in a seamless way. The approach sketched may be characterized as event-centered.

Structural versus behavioral encapsulation

Object-oriented modeling has clearly been inspired by or, to be more careful, shows significant similarity to the method of semantic modeling that has become popular for developing information systems. In an amusing paper,  [Ki89] discusses how semantic modeling and object-oriented modeling are related. Apart from a difference in terminology, semantic modeling differs from object-oriented modeling primarily by its focus on structural aspects, whereas object-oriented modeling is more concerned with behavioral aspects, as characterized by the notion of responsibilities. Typically, semantic modeling techniques provide a richer repertoire for constructing types, including a variety of methods for aggregation and a notion of grouping by association. See slide 3-semantic. The object-oriented counterpart of aggregation may be characterized as the has-a or part-of relation, that is usually expressed by including the (part) object as a data member. Associations between objects cannot be expressed directly in an object-oriented framework. On an implementation level, the association relation corresponds to membership of a common collection, or being stored in the same container. However, the absence of an explicit association relation makes it hard to express general m-n relations, as, for example, the relation between students and courses.

Object-oriented modeling

slide: Relations between objects

The influence of a semantic modeling background can be clearly felt in the OMT method. The object model of OMT is a rather direct generalization of the entity-relationship model. Entities in the entity-relationship model may only contain (non-object) data members, which are called attributes.

In contrast, objects (in the more general sense) usually hide object and non-object data members, and instead provide a method interface. Moreover, object-oriented modeling focuses on behavioral properties, whereas semantic modeling has been more concerned with (non-behavioral) data types and (in the presence of inheritance) data subtypes.

Relations, as may be expressed in the entity-relationship model, can partly be expressed directly in terms of the mechanisms supported by object-oriented languages. For instance, the is-a relation corresponds closely (although not completely) with the inheritance relation. See slide 3-challenges. Both the has-a and uses relation is usually implemented by including (a pointer to) an object as a data member. Another important relation is the is-like relation, which may exist between objects that are neither related by the inheritance relation nor by the subtype relation, but yet have a similar interface and hence may be regarded as being of analogous types. The is-like relation may be enforced by parametrized types that require the presence of particular methods, such as a compare operator in the case of a generic list supporting a sort method.

Model-based specification

State and operations


  • $state == [ decls | constraints ]$
  • $op == [ %D state; decls | constraints ]$

Change and invariance

  • $ %D state == state /\ state' $
  • $ %X state == state = state' $


  • $ state /\ pre( op ) => op $

slide: Model-based specification

Several development methods, including Responsibility Driven Design and Fusion (see section Fusion), allow for the specification of user interactions in a semi-formal way by means of pre- and post-conditions. These approaches have been inspired by model-based specification methods such as VDM and Z, which offer a formal framework for specifying the requirements of a system. Model-based specification methods derive their name from the opportunity to specify a mathematical model capturing the relevant features of the system. Operations, which may correspond to user actions, can then be specified in a purely logical way.

In the following, an outline of the specification language Z will be given. More importantly, the specification of a simple library system will be discussed, illustrating how we may specify user actions in an abstract way. (The use of the Z specification language is in this respect only of subsidiary importance.) In the subsequent section, we will look at the realization of the library employing an abstract system of objects and events corresponding to the user actions, which reflects the characterization given in the formal specification. The specification language Z is based on classical (two-valued) logic and set theory. It has been used in a number of industrial projects,  [Hayes92], and to specify the architecture of complex intelligent systems,  [Craig91]. The central compositional unit of specification in Z is the schema. A schema may be used to specify both states and operations in a logical way. The logic employed in Z is a typed logic. The specification of a schema consists of a number of declarations followed by constraints specifying conditions on the variables introduced in the declarations. Declarations may include other schemas, as in the example specification of the operation op. The schema $%D state$ itself is a compound schema that results from the logical conjunction of the schema state and its primed version $state'$, which denotes state after applying op. Both schema inclusion and schema conjunction are examples of the powerful schema calculus supported by Z, which enables the user to specify complex systems in Z. Moreover, schemas may be decorated to specify the effects of an operation. Invariance may be specified as in $%X state$, which expresses that the state before applying the operation is the same as the state (denoted by $state'$) after applying the operation. Since schemas are specified in a logical manner, both pre- and post-conditions are implicitly specified by the constraints included in the schema. Hence, to verify that an operation op is legal for a state it is merely required to verify that the conditions specified for state hold, and that, together with the pre-conditions (which are implicitly specified by the schema for op), they imply the logical formula characterizing op. See slide 10-model.



  n : \nat
  n \geq 0


  \Delta Counter
  \mbox{ $ n' = n + 1 $ }
  \Delta Counter
  n > 0 \\
  \mbox{ $ n' = n - 1 $ }

slide: The specification of a Counter in Z

An important property of Z is that it allows for a graphical layout of schemas, as illustrated in the specification of a Counter given in slide z-ctr. The state of a Counter is given by the Counter schema declaring an integer variable n, which is constrained by the condition $ n \geq 0 $. The operations Incr and Decr are specified by defining the state following the operation by, respectively, $ n' = n + 1 $ and $ n' = n - 1 $. Both operations require the declaration $%D Counter$ to indicate that the state specified by Counter will be modified. In addition, the operation Decr requires as a pre-condition that $n > 0$, needed to prevent the violation of the invariant, which would happen whenever n became less than zero.



   $Counter \defs [ n : \nat | n \geq 0 ] $
   $Counter::Incr \defs [ \%D Counter, v? : \nat | n' = n + v? ]$
   $Counter::Decr \defs [ \%D Counter | n > 0;  n' = n - 1 ]$
   $Counter::Value \defs [ \%X Counter; v! : \nat | v! = n ]$

Bounded counter

   $Bounded::Counter \defs [ Counter | n \leq Max ]$
   $Bounded::Incr \defs [ Counter::Incr | n < Max ]$

slide: An alternative specification of the Counter

An alternative specification of the Counter is given in slide z-ctr-2. To emphasize that we may regard the Counter as an object, the operations have been prefixed by Counter in a C++-like manner. This is only a syntactic device, however, carrying no formal meaning. In addition, both the operations Incr and Decr declare an integer variable $v?$ which acts, by convention, as an input parameter. Similarly, the integer variable $v!$ declared for the operation value acts, again by convention, as an output parameter. Since Z allows the inclusion of other schemas in the declaration part of a schema, we may easily mimic inheritance as illustrated in the specification of $Bounded::Counter$, which is a Counter with a maximum given by an integer constant $Max$.

Similarly, we may specify the operations for the $Bounded::Counter$ by including the corresponding operations specified for the Counter, adding conditions if required.

From a schema we may easily extract the pre-conditions for an operation by removing from the conditions the parts involving a primed variable. Clearly, the post-condition is then characterized by the conditions thus eliminated.

For example, the pre-condition of the $Counter::Incr$ operation is $v? \geq 0$, whereas the post-condition is $n' = n + v?$ which corresponds to the implementation requirement that the new value of the Counter is the old value plus the value of the argument $v?$. In a similar way, the pre-condition for applying the $Bounded::Incr$ operation is $n + v? \leq Max$. Note, however, that this pre-condition is stronger than the original pre-condition $v? \geq 0$, hence to conform with the rules for refinement we must specify what happens when $ n + v? > Max $ as well. This is left as an exercise for the reader.

Clearly, although Z lacks a notion of objects or classes, it may conveniently be employed to specify the behavior of an object. In  [Stepney], a number of studies are collected which propose extending Z with a formal notion of classes and inheritance. The reader interested in these extensions is invited in particular to study Object-Z, OOZE and Z++. As an historical aside, we may note that Z has been of significant influence in the development of Eiffel (see Meyer, 1992b). Although the two approaches are quite divergent, they obviously still share a common interest in correctness.

In contrast to Eiffel, which offers only a semi-formal way in which to specify the behavior of object classes, Z allows for a precise formal specification of the requirements a system must meet. To have the specification reflect the object structure of the system more closely, one of the extensions of Z mentioned above may be used. An example of using (plain) Z to specify the functionality of a library system is given below.

The specification of a library

Imagine that you must develop a program to manage a library, that is keep a record of the books that have been borrowed.


Library (1)

  books : \power Book \\
  borrowed : Book \pfun Person
  \dom borrowed \subseteq books

slide: The specification of a library

Before developing a detailed object model, you may well reflect on what user services the library must provide. These services include the borrowing of a book, returning a book and asking whether a person has borrowed any books, and if so which books. These operations are specified by the schemas Borrow, Return and Has in slide z-lib-2.


Library (2)

  \Delta Library; b? : Book; p? : Person
  b? \not\in \dom borrowed \\
  b? \in books \\
  borrowed' \mbox{ $ = $ } borrowed \cup { b? \mapsto p? }
  \Delta Library; b? : Book; p? : Person
  b? \in \dom borrowed \\
  borrowed' \mbox{ $ = $ } borrowed \hide { b? \mapsto p? }
   \Xi Library; p? : Person; bks : \power Book
  bks! \mbox{ $ = $ } borrowed ^{-1} \limg { p? } \rimg

slide: The library operations

Don't be frightened of the mathematical notation in which these operations are specified. The notation is only of secondary importance and will be explained as we go along. Since we are only interested in the abstract relations between people and books, we may assume Book and Person to be primitive types. The specification given in slide z-lib-1 specifies an abstract state, which is actually a partial function delivering the person that borrowed the book if the function is defined for the book. The function is partial to allow for the situation where a book has not been borrowed, but still lies on the shelves. The invariant of the library system states that the domain of the function borrowed must be a subset of the books available in the library. Given the specification of the state, and some mathematical intuition, the specification of the operations is quite straightforward. When a Borrow action occurs, which has as input a book $b?$ and a person $p?$, the function $borrowed'$ is defined by extending borrowed with the association between $b?$ and $p?$, which is expressed as the mapping $b? |-> p?$. As a pre-condition for Borrow, we have that borrowed must not be defined for $b?$, otherwise some person would already have borrowed the book $b?$. The Return action may be considered as the reverse of the Borrow action. Its pre-condition states that borrowed must be defined for $b?$ and the result of the operation is that the association between $b?$ and $p?$ is removed from $borrowed '$. Finally, the operation Has allows us to query what books are in the possession of a person $p?$. The specification of Has employs the mathematical features of Z in a nice way. The output, which is stored in the output parameter $bks!$, consists of all the books related to the person $p?$. The set of books related to $p?$ is obtained by taking the relational image of the inversion of borrowed for the singleton set consisting of $p?$, that is, each book x for which an association $ x |-> p? $ is in borrowed is included in the set $bks!$. Again, it is not the notation that is important here, but the fact that the specification defines all top-level user interactions.

Abstract systems and events

User actions may require complex interactions between the objects constituting the object model of a system. Such interactions are often of an ad hoc character in the sense that they embody one of the many possible ways in which the functionality of objects may be used. What we need is a methodology or paradigm that allows us to express these interactions in a concise yet pragmatically amenable way. In  [Henderson93], a notion of abstract systems is introduced that seems to meet our needs to a large extent. See slide 3-abstract.

Abstract systems -- design methodology

  • abstract system = abstract data types + protocol

Events -- high level glue

  • realization of the interaction protocol

slide: Abstract systems and events

Abstract systems extend the notion of abstract data types to capture the (possible) interactions between collections of objects. The idea underlying the notion of an abstract system is to collect the commands available for the client or user of the system. The collection of commands comprising an abstract system are usually a (strict) subset of the commands available in the combined interface of the abstract data types involved. In other words, an abstract system provides a restricted interface, restricted to safeguard the user from breaking the protocol of interaction implicitly defined by the collection of abstract data types of which the system consists. An abstract system in itself merely provides a guideline on how a collection of objects is to be used, but does not offer a formal means to check whether a user plays by the rules. After presenting an example of an abstract system, we will look at how events may be used to protect the user against breaking the (implicit) laws governing the interaction.

Example -- the library

The abstract system comprising a library may be characterized as in slide 3-library. In essence, it provides an exemplary interface, that is, it lists the statements that are typically used by a client of the library software. We use typical identifiers to denote objects of the various types involved.

Abstract system -- exemplary interface


  p = new person();
  b = new book();
  p = b->borrower;
  s = p->books;
  tf = b->inlibrary();

For person* p; book* b; set<book>* s; bool tf;

slide: The library system

The commands available to the user of the library software are constructors for a person and a book, an instruction to get access to the borrower of a particular book, an instruction to ask what books a particular person has borrowed, an instruction to query whether a particular book is in the library, and instructions for a person to borrow or return a book. To realize the abstract system library, we evidently need the classes book and person. The class book may be defined as follows.

  class book { 
public: person* borrower; book() {} void borrow( person* p ) { borrower = p; } void _return( person* p ) { borrower = 0; } bool inlibrary() { return !borrower; } };
It consists of a constructor, functions to borrow and return a book, a function to test whether the book is in the library and an instance variable containing the borrower of the book. Naturally, the class book may be improved with respect to encapsulation (by providing a method to access the borrower) and may further be extended to store additional information, such as the title and publisher of the book.

  class person { 
public: person() { books = new set(); } void allocate( book* b ) { books->insert(b); } void deallocate( book* b ) { books->remove(b); } set* books; };
The next class involved in the library system is the class person, given above. The class person offers a constructor, an instance variable to store the set of books borrowed by the person and the functions allocate and deallocate to respectively insert and remove the books from the person's collection. A typical example of using the library system is given below.

  book* Stroustrup = new book(); 
book* ChandyMisra = new book(); book* Smalltalk80 = new book(); person* Hans = new person(); person* Cees = new person(); Stroustrup->borrow(Hans); Hans->allocate(Stroustrup); ChandyMisra->borrow(Cees); Cees->allocate(ChandyMisra); Smalltalk80->borrow(Cees); Cees->allocate(Smalltalk80);
First, a number of books are defined, then a number of persons, and finally (some of) the books that are borrowed by (some of) the persons.

Note that lending a book involves both the invocation of $book::borrow$ and $person::allocate$. This could easily be simplified by extending the function $book::borrow$ and $book::_return$ with the statements $p->allocate(this)$ and $p->deallocate(this)$ respectively. However, I would rather take the opportunity to illustrate the use of events, providing a generic solution to the interaction problem noted.


 [Henderson93] introduces events as a means by which to control the complexity of relating a user interface to the functionality provided by the classes comprising the library system. The idea underlying the use of events is that for every kind of interaction with the user a specific event class is defined that captures the details of the interaction between the user and the various object classes. Abstractly, we may define an event as an entity with only two significant moments in its life-span, the moment of its creation (and initialization) and the moment of its activation (that is when it actually happens). As a class we may define an event as follows.

  class Event { 
public: virtual void operator()() = 0; };
The class $Event$ is an abstract class, since the application operator that may be used to activate the event is defined as zero.

  class Borrow : public Event { 
public: Borrow( person* _p, book* _b ) { _b = b; _p = p; } void operator()() { require( _b && _p ); // _b and _p exist _b->borrow(p); _p->allocate(b); } private: person* _p; book* _b; };
For the library system defined above we may conceive of two actual events (that is, possible refinements of the $Event$ class), namely a Borrow event and a Return event.

The Borrow event class provides a controlled way in which to effect the borrowing of a book. In a similar way, a Return event class may be defined.

  class Return : public Event { 
public: Return( person* _p, book* _b ) { _b = b; _p = p; } void operator()() { require( _b && _p ); _b->_return(p); _p->deallocate(b); } private: person* _p; book* _b; };
The operation Has specified in the previous section has an immediate counterpart in the $person::books$ data member and need not be implemented by a separate event.

Events are primarily used as intermediate between the user (interface) and the objects comprising the library system. For the application at hand, using events may seem to be somewhat of an overkill. However, events not only give a precise characterization of the interactions involved but, equally importantly, allow for extending the repertoire of interactions without disrupting the structure of the application simply by introducing additional event types.

(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.