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()
- enable contract checking
import contract contract.checkmod(__name__)
def _test():
import doctest, sort return doctest.testmod(sort)
if __name__ == "__main__":
_test()