CSC/ECE 517 Fall 2007/wiki3 2 at

Topic:
In class, we had some difficulty coming up with good examples of programming by contract. Find some concise ones that illustrate the principle well, and are accessible to a general audience of programmers.

Programming by contract

Programming by Contract is a way of specifying the behavior of a function, and the name arises from its formal similarity to a legal contract. The key concept is viewing the relationship between a class and its clients as a formal agreement, expressing each party’s rights and obligations. Defining a precondition and a postcondition for a routine is a way to define a contract that binds the routine and its callers. The precondition states the properties that must hold whenever the routine is called; the postcondition states the properties that the routine guarantees when it returns.
By associating clauses require pre and ensure post with a routine r, the class tells its clients:

If you promise to call r with pre satisfied then I, in return, promise to deliver a final state in which post is satisfied.

Consider the following example:

Stack Example: [1]

class STACK [G] feature  
 ...Declaration of the features:
    count, empty, full, put, remove, item
end

Before considering implementation issues, however, it is important to note that the routines are characterized by strong semantic properties, independent of any specific representation.

For example:
• Routines remove and item are only applicable if the number of elements is not zero.
• put increases the number of elements by one; remove decreases it by one.

Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software.

We will express preconditions and postconditions as clauses of routine declarations introduced by the keywords require and ensure respectively. For the stack class, leaving the routine implementations blank, this gives [1]:

Stack Example: [1]

class STACK1 [G] feature -- Access
     count: INTEGER
            -- Number of stack elements
     item: G is
                 -- Top element
            require
            not empty
            do
               .... 
            end

feature -- Status report
     empty: BOOLEAN is
                 -- Is stack empty?
            do 
               ....
            end

     full: BOOLEAN is
                 -- Is stack representation full?
            do
               ....     
            end

feature -- Element change
     put (x: G) is
                 -- Add x on top. 
            require
                not full
            do
                .... 
            ensure
                not empty
                item = x
                count = old count + 1
            end

     remove is
                  -- Remove top element.
            require
                not empty
            do
                .... 
            ensure
                not full
                count = old count – 1
            end
end

Both the require and the ensure clauses are optional; when present, they appear at the places shown. The require appears before the local clause, if present.

Preconditions: A precondition expresses the constraints under which a routine will function properly.
Here:
• put may not be called if the stack representation is full.
• remove and item may not be applied to an empty stack.

A precondition applies to all calls of the routine, both from within the class and from clients. A correct system will never execute a call in a state that does not satisfy the precondition of the called routine.

Postconditions A postcondition expresses properties of the state resulting from a routine’s execution.
Here:
• After a put, the stack may not be empty, its top is the element just pushed, and its number of elements has been increased by one.
• After a remove, the stack may not be full, and its number of elements has been decreased by one.
The presence of a postcondition clause in a routine expresses a guarantee on the part of the routine’s implementor that the routine will yield a state satisfying certain properties, assuming it has been called with the precondition satisfied.

A precondition-postcondition pair for a routine will describe the contract that the routine (the supplier of a certain service) defines for its callers (the clients of that service).
The following will be true for contracts between classes:
• The precondition binds the client: it defines the conditions under which a call to the routine is legitimate. It is an obligation for the client and a benefit for the supplier.
• The postcondition binds the class: it defines the conditions that must be ensured by the routine on return. It is a benefit for the client and an obligation for the supplier.

The benefits are, for the client, the guarantee that certain properties will hold after the call; for the supplier, the guarantee that certain assumptions will be satisfied whenever the routine is called. The obligations are, for the client, to satisfy the requirements as stated by the precondition; for the supplier, to do the job as stated by the postcondition. Here is the contract for one of the routines in stack example:

A routine contract: routine 'put' for stack class

	OBLIGATIONS	BENEFITS
Client	(Satisfy precondition:) Only call put (x) on a nonfull stack.	(From postcondition:) Get stack updated: not empty, x on top (item yields x, count increased by 1).
Supplier	(Satisfy postcondition:) Update stack representation to have x on top (item yields x), count increased by 1, not empty.	(From precondition:) Simpler processing thanks to the assumption that stack is not full.

Other useful examples

Design By Contract for Java

Contracts for Java (C4J) is a Design By Contract (DBC) framework for Java 1.5 and later. Examples are taken from: [2]

Class invariant example

 @ContractReference(contractClassName = "DummyContract")
  public class Dummy
  {
    protected double m_divisor;

    public Dummy(double divisor)
    {
      m_divisor = divisor;
    }

    public double divide(double x)
    {
      return x / m_divisor;
    }
  }
---------------------------------------------------------
  public class DummyContract
  {
    Dummy m_target;

    public DummyContract(Dummy target)
    {
      m_target = target;
    }

    public void classInvariant()
    {
      assert m_target.m_divisor != 0;
    }
  }

The Dummy class constructor in this example makes an assumption that parameter divisor is never 0.
This is verified by the classInvariant method in the DummyContract class. The contract is tied to
the target using an annotation. The contract has a constructor that takes an argument of the target
type. The contractClassName attribute of the ContractReference annotation does not have to be fully
qualified if the contract class is implemented in the same package as the target class.

Pre condition example

  @ContractReference(contractClassName = "DummyContract")
  public class Dummy
  {
    public double divide(double x, double y)
    {
      return x / y;
    }
  }
---------------------------------------------------------------
  public class DummyContract
  {
    public void classInvariant()
    {
      // Nothing to do here
    }

    public void pre_divide(double x, double y)
    {
      assert y != 0;
    }
  }

In this example, in the divide method, it is assumed that the value of y will never be 0. 
This is verified in the pre_divide method in the DummyContract class.

Interface example

  @ContractReference(contractClassName = "DummyContract")
  public interface Dummy
  {
    double divide(double x, double y);
  }
------------------------------------------------------------
  public class DummyContract extends ContractBase<Dummy>
  {
    public DummyContract(Dummy target)
    {
      super(target);
    }

    public void pre_divide(double x, double y)
    {
      assert y != 0;
    }

    public void post_divide(double x, double y)
    {
      assert getReturnValue() == x / y;
    }
  }

In this example, the contract will verify that all the usages of the divide interface meets the
precondition, and that all implementations of the interface will meet the post condition.

Design by Contract Programming in C++

The material in this section has been taken from: [3]

Design by Contract Framework

// Object class is the base class for all
// objects in the system. All classes inheriting from this class need 
// to define a method IsValid. This method should perform a
// consistency check on the state of the object. Note that 
// this method needs to be defined only when a debug build is made
class Object
{
public:
#ifdef _DEBUG
    bool IsValid() const = 0;
#endif
    
};

#ifdef _DEBUG

// The debug mode also defines the following macros. Failure of any of these macros leads to
// program termination. The user is notified of the error condition with the right file name
// and line number. The actual failing operation is also printed using the stringizing operator #

#define ASSERT(bool_expression) if (!(bool_expression)) abort_program(__FILE__, __LINE__, #bool_expression)
#define IS_VALID(obj) ASSERT((obj) != NULL && (obj)->IsValid())
#define REQUIRE(bool_expression) ASSERT(bool_expression)
#define ENSURE(bool_expression) ASSERT(bool_expression)

#else

// When built in release mode, the _DEBUG flag would not be defined, thus there will be no overhead
// in the final release from these checks.

#define ASSERT(ignore) ((void) 0)
#define IS_VALID(ignore) ((void) 0) 
#define REQUIRE(ignore) ((void) 0)
#define ENSURE(ignore) ((void) 0)

#endif

Example: Terminal Manager

Terminal Manager exemplifies a typical design pattern seen in embedded systems. Here a collection of terminals is being managed by the Terminal Manager. Management involves routing messages, creating and deleting terminals.
The Terminal Manager implements the following methods:

   a)Add_Terminal: Create and add a new terminal

   b)Remove_Terminal: Remove and delete a terminal

   c)Find_Terminal: Find a terminal from its terminal_Id

   d)Handle_Message: Route the received message to the Terminal object

#include <map>      // Header file include for map
using std;          // STL containers are defined in std namespace

class TerminalManager : public Object
{
   // The map is keyed with the terminal id and stores pointers to Terminals.
   // terminal id is an integer, terminal ids can be in the entire range for
   // an integer and they will still be efficiently stored inside a map.
   typedef map<int, Terminal *> TerminalMap;
   TerminalMap m_terminalMap;
   int m_managerType;
   FaultManager m_faultManager;

public:

#ifdef _DEBUG
   // IsValid methods play an important role in checking the consistency
   // of objects in the debug. IsValid is defined as a pure virtual function
   // in Object class, thus it needs to be overriden in all inheriting classes.
   // The inheriting class should perform defensive checks to make
   // sure that it is in a consistent state/
   // Also note that this method is only available in the debug build.
   virtual bool IsValid() const
   {
       return (m_terminalMap.count() <= MAX_TERMINALS_PER_MANAGER &&
               m_managerType < MAX_MANAGER_TYPES &&
               m_faultManager.IsValid());  
   }
   
#endif

   Status AddTerminal(int terminalId, int type)
   {
      // Checking Preconditions
      REQUIRE(terminalId < MAX_TERMINAL_ID);
      REQUIRE(type >= TERMINAL_TYPE_RANGE_MIN && type <= TERMINAL_TYPE_RANGE_MAX);
      
      Status status;
      
      // Check if the terminal is already present in the map. count()
      // returns the total number of entries that are keyed by terminalId
      if(m_terminalMap.count(terminalId) == 0)
      {
         // count() returned zero, so no entries are present in the map
         Terminal *pTerm = new Terminal(terminalId, type);
 
         // Make sure that the newly created terminal is in consistent state
         IS_VALID(pTerm);
         
         // Since map overloads the array operator [ ], it gives 
         // the illusion of indexing into an array. The following
         // line makes an entry into the map
         m_terminalMap[termId] = pTerm;
         
         status = SUCCESS;
      }
      else
      {
         // count() returned a non zero value, so the terminal is already
         // present.
         status = FAILURE;
      }
      
      // Checking post conditions:
      // 1. TerminalManager should be consistent
      // 2. The new terminal should always be found
      // 3. The manager should not be controlling more terminals
      //    than allowed
      // 4. Make sure correct return code is being returned.
      IS_VALID(this);
      ENSURE(FindTerminal(termId));
      ENSURE(m_terminalMap.count() <= MAX_TERMINALS_PER_MANAGER));
      ENSURE(status == SUCCESS || status == FAILURE);
      return status;
   }
   
   Status RemoveTerminal(int terminalId)
   {
      // Check pre-conditions
      // Note: Here the REQUIRE macro makes sure that
      // terminal to be deleted is actually present. A similar
      // check will be done in the main body of the code.
      // The duplicate check in the REQUIRE macro allows flagging
      // the error earlier.

      REQUIRE(terminalId < MAX_TERMINAL_ID);
      REQUIRE(FindTerminal(terminalId));
      
      Status status;
      // Check if the terminal is present
      if (m_terminalMap.count(terminalId) == 1)
      {
         // Save the pointer that is being deleted from the map
         Terminal *pTerm = m_terminalMap[terminalId]; 
      
         // Make sure that terminal object being deleted is in a consistent
         // state
         IS_VALID(pTerm);         
   
         // Erase the entry from the map. This just frees up the memory for
         // the pointer. The actual object is freed up using delete
         m_terminalMap.erase(terminalId);
         delete pTerm;
         
         status = SUCCESS;
      }
      else
      {
         status = FAILURE;
      }

      // Checking Post-conditions:
      // 1. Terminal has been successfully deleted (terminal find
      //    should return NULL)
      // 2. Only valid status should be returned.
      // 3. Terminal Manager is in a consistent state
      ENSURE(FindTerminal(terminalId) == NULL);
      ENSURE(status == SUCCESS || status == FAILURE);
      IS_VALID(this);     
      
      return status;
   }
  
  // Find the terminal for a given terminal id, return
  // NULL if terminal not found
  Terminal *FindTerminal(int terminalId)
  {
     Terminal *pTerm;
     if (m_terminalMap.count(terminalId) == 1)
     {
        pTerm = m_terminalMap[terminalId];
     }
     else
     {
         pTerm = NULL;
     }
     
     return pTerm;
  } 
  
  void HandleMessage(const Message *pMsg)
  {
     // Check pre-conditions:
     IS_VALID(pMsg);
     ENSURE(FindTerminal(pMsg->GetTerminal()));
     
     int terminalId = pMsg->GetTerminalId();
     
     Terminal *pTerm;
     
     pTerm = FindTerminal(terminalId);
     
     if (pTerm)
     {
        pTerm->HandleMessage(pMsg);
     }    
  }
};

More good examples can be found at the sites mentioned below

http://en.wikibooks.org/wiki/Computer_programming/Design_by_Contract
http://www.eventhelix.com/RealtimeMantra/Object_Oriented/design_by_contract.htm
http://www.cs.uno.edu/~c1581/Labs2006/lab7/lab7.htm
http://www.phpunit.de/pocket_guide/3.2/en/test-first-programming.html
http://www.python.org/dev/peps/pep-0316/
http://www.artima.com/cppsource/deepspace2.html
http://java.sun.com/j2se/1.4.2/docs/guide/lang/assert.html
http://www.csc.calpoly.edu/~dstearns/SeniorProjectsWWW/Rideg/dbc.html
http://taipei-jackie.info/Slides/presentation_slides_2.ppt
http://www.ibm.com/developerworks/rational/library/455.html#N10324

References

[1] Object-Oriented Software Construction SECOND EDITION.
[2] http://c4j.sourceforge.net/
[3] http://www.eventhelix.com/RealtimeMantra/Object_Oriented/design_by_contract.htm