Programming by Contract

Purpose of this Wiki

This wiki page was created to address the following assignment:

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.

Per the assignment to find examples, all examples were drawn from outside sources and put into this wiki with mainly only formatting changes.

Overview

Programming by Contract originated with the Eiffel programming language. ¹ It is a technique for designing software systems in such a way that all the pieces meet certain obligations to each other. If all obligations are correctly met, then the system as a whole will work correctly.

The obligations are defined in terms of suppliers (components that offer a method that can be invoked) and clients (components that invoke those methods). Suppliers must provide the service they are contracted to provide, and clients must respect the restrictions of the supplier. The contract is enforced through preconditions and postconditions. A precondition is a definition of the state of the system and parameters prior to invoking a service. The client must ensure they have met the preconditions required by the supplier, or else the supplier's behavior is undefined. A postcondition is a definition of the state of the system and return value after the service invocation is complete. The supplier must ensure that if the precondition was met, then the postcondition is met so that the client gets back a result that conforms to the postcondition.

It is important to note that programming by contract is more than a design approach. It can be enforced by the language itself to ensure that all code is written with an understanding of the contract (as opposed to simply specifying the assumed contract obligations in a comment at the top of a method).

Examples

Real World Examples

Examples in this section are based around real world metaphors and do not rely on programming specific concepts such as classes, methods, etc.

This example examines the process of scheduling a vacation in terms of the various suppliers and clients required to send an individual on a trip and the contracts between each.
Example taken from http://en.wikipedia.org/wiki/Design_by_contract

Take the process of going on holiday, for example. Bertrand wants to spend two weeks in Florida. He books the
holiday through DBC Holidays Inc., who specialise in U.S. package holidays. When he makes the booking
(collaboration #1), Bertrand is the client and DBC Holidays are the supplier. DBC Holidays then arrange flights
through Assertair Corp. (collaboration #2), and book a room at the Precondition Plaza Hotel in Miami
(collaboration #3). In collaboration #2, DBC Holidays are the client and Assertair is the supplier, and in
collaboration #3, the hotel is the supplier. And the chain of collaborations goes deeper and deeper (e.g., who
does Assertair pay to service their jets?)

If any link in this chain of collaborations breaks, then the result could be that Bertrand's holiday is ruined.
It's vital, therefore, that every player in the collaboration does what they're supposed to do. In any
collaboration, client and supplier have certain obligations. These obligations (or "responsibilities", if you
like) fall into three distinct types:

1. Things that the supplier promises to do as part of the service it offers to the client (e.g., Assertair
promises DBC Holidays that Bertrand will be in Miami at a certain date and time)
2. Things that the client promises to do before using the service (e.g., DBC Holidays must ensure that
Bertrand has his passport and tickets when he checks in for his flight)
3. Things that the supplier promises will always be true no matter what happens (e.g., The airline will
always have adequate insurance to cover any accident)

Things that the supplier promises to do as part of the service are described as a special kind of rule called a
postcondition. The postcondition tells the client what will be true if the service is executed correctly (e.g.,
"your customer will be in Miami by 15:30 on June 8").

If Bertrand turns up at the check-in desk without his passport, of course, then the airline can't live up to its
side of the contract: he will not be allowed to board the plane without it. A rule that the client must satisfy
before using a service is called a precondition.

A rule that states what must always be true is called an invariant. If the airline doesn't have adequate
insurance then nobody is going anywhere!

Another airline based example with a slightly different set of contracts. Example from http://archive.eiffel.com/doc/manuals/technology/contract/

	Obligations	Benefits
Client	Be at the Santa Barbara airport at least 5 minutes before scheduled departure time. Bring only acceptable baggage. Pay ticket price. (precondition)	Reach Chicago. (postcondition)
Supplier	Bring customer to Chicago. (postcondition)	No need to carry passenger who is late, has unacceptable baggage, or has not paid ticket price. (precondition)

A sample contract for a postal service. Example from http://se.ethz.ch/~meyer/publications/computer/contract.pdf

	Obligations	Benefits
Client	Provide letter or package of no more than 5 kgs, each dimension no more than 2 meters. Pay 100 francs. (precondition)	Get package delivered to recipient in four hours or less. (postcondition)
Supplier	Deliver package to recipient in four hours or less. (postcondition)	No need to deal with deliveries too big, too heavy, or unpaid. (precondition)

Programming Based Examples

Examples in this section use terms which are more specific to programming, defining themselves in terms of classes, methods, and code. In keeping with the goal of having the examples be accessible to the general audience of programmers, examples using exotic/rare programming languages were excluded.

In this Java example a Stack class is defined in Java as a supplier of certain methods. It's contractual obligations are specified in the comments of each method as either requirements (contractual obligations on the client) or ensure statements (assurances about the state of the system after the method is invoked. i.e. preconditions)

Example from: http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html

class Stack {  // supplier
  Object[] data = null;

  int top = -1;
  int n = 0;

  public Stack(int n)
    // require n>0;
  {
    this.n = n;
    data = new Object[n];
  }

  public void push(Object o)
    // require top<(n-1);
    // ensure top==o;
    // ensure top = old top + 1;
  {
    top++;
    data[top] = o;
  }

class Main { // client
  public static void main(String[] args) {
    Stack s = new Stack(10);
    s.push("Apple");
  }
}

This example covers the pre and post conditions of a program which maintains a dictionary. Example from http://archive.eiffel.com/doc/manuals/technology/contract/

	Obligations	Benefits
Client	Make sure table is not full and key is a non-empty string. (precondition)	Get updated table where the given element now appears, associated with the given key. (postcondition)
Supplier	Record given element in table, associated with given key. (postcondition)	No need to do anything if table is full, or key is empty string. (precondition)

This example analyzes the C strcpy() function in terms of what preconditions/postconditions it can assert. Example drawn from http://www.artima.com/cppsource/deepspace.html

// preconditions
// - src points to a sequence of N + 1 characters (type char) each of whose value is accessible by 
//   the expression *(src + n), where n is an integer in the range [0, N + 1)
// - dest points to a block of memory that is writable for a length of N + 1 (or more) characters 
// postconditions
// - For each n in the range [0, N + 1), the expression *(src + n) == *(dest + n) holds true
// - The value returned is the value passed in the dest parameter 
char *strcpy(char *dest, char const *src)
{
  char *const r = dest;
  for(;; ++dest, ++src)
  {
    if(�\0� == (*dest = *src))
    {
       break;
    }
  }
  return r;
}

An example of the contract for a list sorting method. Although the code itself is in python, the general concepts of what sort of things need to be asserted for a sort method are valid regardless of the programming language. Example from http://www.wayforward.net/pycontract/

def sort(a):
    """Sort a list *IN PLACE*.

    pre:
        # must be a list
        isinstance(a, list)

        # all elements must be comparable with all other items
        forall(range(len(a)),
               lambda i: forall(range(len(a)),
                                lambda j: (a[i] < a[j]) ^ (a[i] >= a[j])))

    post[a]:
        # length of array is unchanged
        len(a) == len(__old__.a)

        # all elements given are still in the array
        forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))

        # the array is sorted
        forall([a[i] >= a[i-1] for i in range(1, len(a))])
    """