A class invariant is a Boolean condition on a class’s state that must hold after construction and before and after every state-changing method. It prevents objects from remaining in invalid states. The condition may be temporarily false during mutation, but must be restored before the method returns. section 6.3.4
Apply the principle by:
- Expressing the valid relationship among instance variables. section 6.3.4
- Checking the condition after construction and after each method that mutates state. section 6.3.4
- Using assertions or exceptions to expose violations instead of leaving invalid objects available to callers. section 6.3 section 6.4
Circular buffer
For a circular buffer, the invariant is `(0 <= _head < _capacity) and (0 <= _tail < _capacity)`. Initialization sets both indexes to zero; add() and remove() advance them with modulo capacity, preserving the bounds. An assertion checks the invariant when the object is created and when mutating methods return. section 6.3.1 section 6.3.4
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 Python CircularBuffer implementation, including its invariant method, constructor assertion, and method contracts. section 6.3.1
