Programming by contract makes a component’s obligations explicit through preconditions, postconditions, and class invariants. The resulting agreement reduces runtime surprises for callers and users. section 6.0 section 6.3
Apply the contract through three complementary obligations:
- Check a precondition before calling a method. The caller is responsible for ensuring that the condition is true; otherwise, the method need not behave conveniently. section 6.3.2
- Guarantee a postcondition before returning when the precondition was satisfied. The caller can then rely on successful behavior or on the specified exception contract. section 6.3.3
- Maintain a class invariant before and after every state-mutating method, preventing objects from being left in invalid states. section 6.3
Circular buffer
A CircularBuffer requires space before add() and stored data before remove(): _count < _capacity and _count > 0. Its invariant keeps _head and _tail within capacity. Assertions check the contract, while client code tests preconditions before making calls. section 6.3.1 section 6.3.2
Listing 6.13 (Program 6.9 CircularBuffer-1): buffer.py
class CircularBuffer:
def _class_invariant(self): #1
return ( (0 <= self._head < self._capacity)
and (0 <= self._tail < self._capacity)
)
def __init__(self, capacity):
self._capacity = capacity
self._head = 0
self._tail = 0
self._count = 0
self._buffer = [0]*capacity
assert self._class_invariant(), \ #2
'class invariant is false' #2
@property
def count(self): return self._count
def add_precondition(self): #3
return self._count < self._capacity
def add_postcondition(self): #4
return self._count > 0
def add(self, value):
assert self.add_precondition(), \ #5
'add_precondition is false' #5
self._buffer[self._tail] = value
self._tail = (self._tail + 1)%self._capacity
self._count += 1
assert self.add_postcondition(), \ #6
'add_postcondition is false' #6
assert self._class_invariant(), \ #7
'class_invariant is false' #7
def remove_precondition(self): #8
return self._count > 0
def remove_postcondition(self): #9
return self._count < self._capacity
def remove(self):
assert self.remove_precondition(), \ #10
'remove_precondition is false' #10
value = self._buffer[self._head]
self._head = (self._head + 1)%self._capacity
self._count -= 1
assert self.remove_postcondition(), \ #11
'remove_postcondition is false' #11
assert self._class_invariant(), \ #12
'class_invariant is false' #12
return value
Inspect the compact Python implementation showing an invariant, method-specific preconditions and postconditions, and assertion-based enforcement. section 6.3.1
Python has no native contract constructs, so assertions, public predicate methods, and exceptions can implement the technique. Use it selectively on critical classes rather than automatically on every class. section 6.3
Inheritance requires compatible contracts: subclass preconditions and postconditions must not conflict with expectations established by the superclass. section 7.5
