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]

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

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. 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" 

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