[3] DejaVU Online: Principles of Object-Oriented Software Development (©)
[3] - [up] [top] - [I] [II] [III] [IV] - [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] - [A] [R]

Specifying contractual obligations

Instructor's Guide

intro, methods, objects, contracts, formal, summary, Q/A, literature
A formal specification of the behavior of an object may be given by defining a pre-condition and post-condition for each method. The pre-condition of a method specifies in a logical manner what restrictions the client invoking a particular method is obliged to comply with. When the client fails to meet these requirements the result of the method will be undefined. In effect, after the violation of a pre-condition anything can happen. Usually, this means that the computation may be aborted or that some other means of error-handling may be started. For instance, when the implementation language supports exceptions an exception handler may be invoked. The post-condition of a method states what obligations the server object has when executing the method, provided that the client's request satisfies the method's pre-condition. Apart from specifying a pre-condition and post-condition for each method publicly supported by the class, the designer of the class may also specify a class invariant, to define the invariant properties of the state of each instance of the class. A class annotated with an invariant and pre- and post-conditions for the methods may be regarded as a contract, since it specifies precisely (in an abstract way) the behavioral conformance conditions of the object and the constraints imposed on the interactions between the object and its clients. See slide 3-obligations.

Assertions -- formal specification

slide: Formal specification of contracts
Intuitively, contracts have a clear analogy to our business affairs in everyday life. For instance, when buying audio equipment, as a client you wish to know what you get for the price you pay, whereas the dealer may require that you pay in cash. Following this metaphor through, we see that the supplier may actually benefit from imposing a (reasonable) pre-condition and that the client has an interest in a well-stated post-condition. Most people are not willing to pay without knowing what they will get for their money.

Language support

 The use of contracts was originally proposed by  [Meyer88], and is directly supported by the language Eiffel, which offers the keywords require (to indicate a pre-condition), ensure (to indicate a post-condition) and invariant (to indicate the invariance condition). See slide 3-formal. The Eiffel environment has options to dynamically check any of the three kinds of assertions, even selectively per class. The assertions, except for the invariance condition, are directly embedded in the code. Although less elegant, the same functionality can be achieved in C++ by using the assert macro defined in {\tt assert.h} as explained in section ASSERT, which also introduced the require and promise macros for C++.

For dynamically checking the invariance condition, a test should be executed when evaluating the constructor and before and after each method invocation. While a method is being executed, the invariant need not necessarily hold, but it is the responsibility of a method to restore the invariant when it is disrupted. In case object methods are recursively applied, the invariant must be restored when returning to the original caller.

An alternative approach to incorporating assertions in a class description is presented in  [Cline], which introduces an extension of C++ called Annotated C++. Instead of directly embedding assertions in the code, Annotated C++ requires the user to specify separately the axioms characterizing the functionality of the methods and their effect on the state of the object.

Interfaces

Contracts may be used to document the method interface of a class. Pre- and post-conditions allow the class designer to specify in a concise manner the functional characteristics of a method, whereas the use of natural language often leads to lengthy (and imprecise) descriptions. Below, an example is given of a contract specifying an account. 
  class account {  
   account  


  public:
  account();
  // assert( invariant() );
  
  virtual float balance() { return _balance; }
  
  void deposit(float x); 
 to deposit money


  // require( x >= 0 );
  // promise( balance()  ==  old_balance  +  x  && invariant() );
  
  void withdraw(float x); 
 to withdraw money


  // require( x  <=  balance() );
  // promise( balance()  ==  old_balance  -  x && invariant() );
  
  bool invariant() { return balance()  >=  0; }
  protected:
  float _balance;
  };
slide: The $account$ contract
The interface for the account class specifies in an abstract way what the user expects of an account. From the perspective of design, the behavioral abstraction expressed by the axioms is exactly what we need, in principle. The implementation must guarantee that these constraints are met.

System development

 From the perspective of system development, the notion of contracts has some interesting consequences. Assertions may be used to decide who is responsible for any erroneous behavior of the system. See slide 3-limits.

System development

A pre-condition limits the cases that a supplier must handle!

slide: System development with contracts
For example, imagine that you are using a software library to implement a system for financial transactions and that your company suffers a number of losses due to bugs in the system. How would you find out whether the loss is your own fault or whether it is caused by some bug in the library? Perhaps surprisingly, the use of assertions allows you to determine exactly whether to sue the library vendor or not. Assume that the classes in the library are all annotated with assertions that can be checked dynamically at runtime. Now, when you replay the examples that resulted in a loss for your company with the option for checking pre- and post-conditions on, it can easily be decided who is in error. In the case that a pre-condition of a method signals violation, you, as a client of a library object, are in error. However, when no pre-condition violation is signaled, but instead a post-condition is violated, then the library object as the supplier of a service is in error; and you may proceed to go to court, or do something less dramatic such as asking the software vendor to correct the bug.

Realization

 The contract specified in the account class interface may actually be enforced in code as illustrated below. 
  class account { 
   account  


  public:
  account() { _balance = 0; assert(invariant()); }
  
  virtual float balance() { return _balance; }
  
  
  void deposit(float x) {
  	require( x >= 0 );  
 check precondition


  	hold(); 
 to save the old state


  	_balance += x; 
  	promise( balance() == old_balance + x );
  	promise( invariant() );
  	}
  
  void withdraw(float x) {
  	require( x <= _balance );  
 check precondition


  	hold(); 
 to save the old state


  	_balance -= x; 
  	promise( balance() == old_balance - x );
  	promise( invariant() );
  	}
  
  virtual bool invariant() { return balance() >= 0; }
  protected:
  float _balance;
  float old_balance; 
 additional variable


  virtual void hold() { old_balance = _balance; }
  };
slide: The realization of the $account$ contract
The additional variable {\em old_balance} is needed to compare the state preceding an operation with the state that results afterwards. The old state must explicitly be copied by calling hold. In this respect, Eiffel offers better support than C++. Whenever balance() proves to be less than zero, the procedure sketched above can be used to determine whether the error is caused by an erroneous method invocation, for example when calling withdraw(x) with x >= balance(), or whether the implementation code contains a bug. For the developer of the software, pre-conditions offer a means to limit the number of cases that a method must be able to handle. Often, programmers tend to anticipate all possible uses. For instance, many programs or systems have options that may be learned only when inspecting the source code but are otherwise undocumented. \nop{See for example [UndocDos].} Rather than providing all possible options, for now and the future, it is more sensible to delineate in a precise manner what input will be processed and what input is considered illegal. For the developer, this may significantly reduce the effort of producing the software.
[3] - [up] [top] - [I] [II] [III] [IV] - [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] - [A] [R]
Hush Online Technology
hush@cs.vu.nl
12/29/99