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]

Examples

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. 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()

1. enable contract checking

import contract contract.checkmod(__name__)

def _test():

   import doctest, sort
   return doctest.testmod(sort)

if __name__ == "__main__":

   _test()

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/