CSC/ECE 517 Fall 2007/wiki3 2 c4

Introduction

Problem

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 (PBC) is also called design by contract. It is a form of progamming that deals with pre conditions, post conditions, and invariants. These are used in a client/supplier model. Pre conditions, post conditons, and invariants are specified first. After that, the code is written based on the specified conditions and invariants. It can be seen as a contract because the code needs to abide by the specifications. These contracts are enforced by assertions.[1] Programming by contract uses assertions to enforce the contract between requirements and code. PBC puts the responsibilities on the client to specify the conditions of the functions and other code to meet while and the supplier to honor these requirements that form a contract. [9]

Implementation and Reasons For

Why Use Programming By Contract?

• PBC helps to define and show the responsibilities of the client and the server. [9]
• Works very well with Inheritance. Any inherited methods need to conform to the contract. [9]
• Able to use assertions to uphold the contract. [9]
• Tests for pre-conditions as well as post-conditions. [9]
• Handles abmormal cases which goes great with exception handling. [10]

How it works

• The client has the responsibility of specifying the post conditions for the supplier.
• The post conditions are used by the supplier to develop code.
• The developed code is then given back to the client with pre-conditions.
• These pre-conditions have to be honored in order for the post conditions to be honored
• This in turn becomes a contract between both sides

Previous information came from reference [9].

Example 1

This example shows design by contract using a sort function. It defines pre and post conditions for the function and also tests the function to make sure that these conditions are upheld. The example below is from link 3.

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

    >>> a = [1, 1, 1, 1, 1, 2, 2, 1]
    >>> sort(a)
    >>> a
    [1, 1, 1, 1, 1, 1, 2, 2]
    >>> a = 'the quick brown fox jumped over the lazy dog'.split()
    >>> sort(a)
    >>> a
    ['brown', 'dog', 'fox', 'jumped', 'lazy', 'over', 'quick', 'the', 'the']

    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))])
    """
    a.sort()

# enable contract checking
import contract
contract.checkmod(__name__)

def _test():
    import doctest, sort
    return doctest.testmod(sort)

if __name__ == "__main__":
    _test()

Example 2

This example is an API example that adds a number to a list. The number has to be between 0 and 100. This example shows different ways of designing by contract. There are three functions and each one defines ever a invariant, pre-condition, or a post-condition. Notice that the assert keyword is used for upholding the contract of each condition. The example below is from link 4.

class SampleTool(StandardTool):

      def _initparms(self):
          self.lst = []

      def _invariant(self):
          assert len(self.lst) < 100

      def addNumber(self, number):
          self.lst.append(number)

      def addNumber_pre_condition(self, number):
          assert type(number) == type(1), "Type must be integer"
          assert (number < 100) and (number > 0), "Number must be less than 100, but greater than 0"

      def length(self):
          return len(self.lst)

      def length_post_condition(self, result):
          assert (result < 100) and (result >= 0), "Result must be less than 100, but greater or equal 0"

Example 3

This is a C++ example of a bar class. The class takes a value but assures that the value is greater than zero. This example is from link 5.

public class Bar
{
  public void m1( int value )
  {
    assert 0 <= value : "Value must be non-negative: value= " + value;
    System.out.println( "OK" );
  }
  public static void main( String[] args )
  {
    Bar bar = new Bar();
    System.out.print( "bar.m1(  1 ): " );
    bar.m1( 1 );
    System.out.print( "bar.m1( -1 ): " );
    bar.m1( -1 );
  }
}

Example 4

This example is written in Java and is an implementation of a stack. Pre and post conditions are implemented as well as an invariant. The example is taken from link 7.

class Stack
{  
   public Stack()
   {  
      objects = new Object[MAX];
      top = 0;
   }
   public void Push(Object o)
   {  
      objects[top] = o;
      top++;
   }
   public Object Pop()
   {  
      top--;
      return  objects[top];
   }
   public int Size()
   {  
      return  top;
   }
   
   private int Remaining()
   {  
      assert (false);
      return  MAX - top;
   }
   
   private Object[] objects;
   private int top;
   private static final int MAX = 10;
   
   preconditions()
   {  
      Push:
      top < MAX;
      Pop:
      top > 0;
   }
   
   postconditions()
   {  
      Push:
      top > 0;
   }
   
   invariants()
   {  
      top >= 0;
      top <= MAX;
   }
}

Example 5

This example is written in Java. Below is two functions that use assertions to check for null and in range. The example is taken from link 8.

/**
 * This method asserts that a specified object is not null.
 * @param object - the object that should not be null.
 * @param name - the name of the object to be used for error reporting.
 */
public final static boolean notNull(Object object, String name) {
	assert object != null: name + " must not be null";
	return true;
}

/**
 * This method asserts that an int value is within a specified range.
 * @param value - the value that must be within the specified range.
 * @param min - the minimum value specified of the specified range.
 * @param max - the maximum value of the specified range.
 * @param name - the name of the value to be used for error reporting.
 */
public final static boolean inRange(int value, int min, int max, String name) {
	assert value >= min && value <= max: name + " must be in the range [" + min + " to " + max + "]. Value is " + value;
	return true;
}

References

1. http://www.dugaldmorrow.com/index.php?option=com_content&task=view&id=19&Itemid=38
2. http://www.javaworld.com/javaworld/jw-02-2001/jw-0216-cooltools.html?page=1
3. http://www.wayforward.net/pycontract/
4. http://pyds.muensterland.org/wiki/programmingbycontractforwebservices.html
5. http://www.javaworld.com/javaworld/jw-11-2001/jw-1109-assert.html?page=2
6. http://www.codeproject.com/csharp/designbycontract.asp
7. http://mozart-dev.sourceforge.net/pi-assert.html
8. http://www.dugaldmorrow.com/index.php?option=com_content&task=view&id=19&Itemid=38
9. http://onestepback.org/index.cgi/Tech/Programming/DbcAndTesting.html
10. http://archive.eiffel.com/doc/manuals/technology/contract/
11. http://www.muc.de/~hoelzl/tools/dbc/dbc.lisp