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