Programming by Contract

Common programming errors

It would not be wrong to say that no software in the world is bug free. A lot of bugs in software can be attributed to the programming errors that the programmers commonly make. The most common of them are: <ref>http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html</ref>

While considering possibilities, the programmer misses out on some
Cut-and-paste programming
Inflexible code that cannot adapt to changes that maybe needed of it in future
Lack of error checking
Software reuse
Lack of mechanisms to recover from errors in a graceful manner

One of the several things essential in making bug free software a reality is "Programming by contract". It helps programmers develop robust software.

Programming by contract

Programming by Contract or Design by Contract (DbC) was first introduced by Bertrand Meyer, the creator of the Eiffel programming language. Although Eiffel has implemented assertions as built in DbC support, the concepts can be applied in any language. It uses pre-conditions and post-conditions to document or programmatically assert the change in state caused by a piece of a program. <ref>http://c2.com/cgi/wiki?DesignByContract</ref>

Background

Programming by Contract or Design by Contract (DbC) has its roots in work on formal verification, formal specification and Hoare logic. The original contributions include:

A clear metaphor to guide the design process.
The application to inheritance, in particular a formalism for redefinition and dynamic binding.
The application to exception handling.
The connection with automatic software documentation. <ref>http://en.wikipedia.org/wiki/Design_by_contract</ref>

Methodology

Programming by Contract creates a contract between the software developer and software user - in Meyer's terms the supplier (callee) and the consumer (caller/client).

Before entering a method or routine, a pre-condition must be satisfied by the consumer of the routine. Each routine ends with a post-conditions which the supplier guarantees to be true (if and only if the preconditions were met). Also, each class has an invariant which must be satisfied after any changes to an object are represented by the class. In other words, the invariant guarantees the object is in a valid state. <ref>http://www.cs.unc.edu/~stotts/204/contract.html</ref>

If the consumer tries to call the method without meeting the preconditions, it can result in unexpected behavior. The program could crash or run in a loop forever. It may also deceptively generate garbage, while giving an impression that it is running correctly.

A Java Example

Here is a Java example that shows where the checks can be placed.

class Supplier{  //the supplier class
  public Supplier()
  {
      //some code that initializes the supplier constructor
      checkInvariant();  //verify class invariant
  }
  public supplier_method(Data data)
  {
     //some actions performed by supplier method
     postCondition(); //check if we have done what has been promised
     checkInvariant(); //verify class invariant
  }
}

class Client { // the client class
  public client_method (Data data){ //client method, calls supplier method
     Supplier s = new Supplier(); //initialize supplier constructor    
     preCondition(data);  //verify the preCondition before calling the supplier method
     s.supplier_method(data);
  }
}

Design by Contract Metaphor

DbC is a metaphor on how elements of a software system collaborate with each other, on the basis of mutual obligations and benefits. The metaphor comes from business life, where a "client" and a "supplier" agree on a "contract" which documents that:

The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).
The client must pay the fee (obligation) and is entitled to get the product (benefit).
Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts. <ref>http://www.eiffel.com/developers/design_by_contract.html</ref>

We can use the previous Java example to show the relationship between obligation and benefit.

	Obligations	Benefit
Client	Satisfy preCondition()	Result from supplier_method
Supplier	Satisfy postCondition()	Know that preCondition() is satisfied by client_method

Apply Programming by Contract to Applications

Inheritance

When programming by contract is used with inheritance, a subcontract is added to the subclass. According to this subcontract and in accordance with the Liskov Substitution Principle <ref>http://www.objectmentor.com/resources/articles/lsp.pdf</ref>, an overridden method in the subclass may have preconditions that are as weak as or weaker than the preconditions of the base class, and postconditions that are as strong as or stronger than the postconditions of the base class. We can see this in the following example:

class A
{
    public int foo(int x)
    {
         assert(1<x<3); // pre-condition
         ...
         assert(result<15); //post-condition
         return result;
    }
}

class B extends A 
{
    public int foo(int x)
    {
         assert(0<x<5); //weakened pre-condition
         ...
         assert(result<3); //strengthened post-condition
         return result;
    }	

}

Exception Handling

When it is necessary to impose restrictions on the input given to a method, rather than just stating preconditions in the documentation, exception handling can be used. If the input, say an argument to the method, is illegal, then an exception can be thrown. This way, the program will work for all inputs. This practice of defending against illegal input is referred to as "Defensive Programming".
The exception handling mechanism helps the user catch errors and handle them appropriately. It also makes sense to use it because the likelihood of errors occurring and illegal input being given to methods is very high. However, the downside to this is that throwing an exception can be very expensive. Let us consider the following example:

class Search
{
    public void BinarySearch(int arr[],int item)
    {         
        Precondition: none
        Postcondition: returns the position of the element to be searched if found, else returns -1
                       If arr[] is not sorted, an IllegalArgumentException is thrown
    }

    public static void main(String args[]) 
    {
        Search s = new Search();
        //define an array in which to find an item
        s.BinarySearch(arr,item); //the method internally handles all inputs
    }  
}

Summary

Design by contract helps programmers identify the consistency conditions that are necessary to the proper functioning of each client-supplier contract, and specify, for each one of the conditions, whose responsibility it is to enforce it. It is advantageous because it reduces the debugging time significantly. It reduces the need for checking errors within the code since it is known that a calling routine will have valid values coming into the routine. Finally, it also provides valuable user documentation that can be extracted by automated tools, e.g. the short tool found in Eiffel implementations).

References

CSC/ECE 517 Fall 2011/ch18 6a sc

Contents