A class invariant is a Boolean condition that must hold after construction and after every public operation changes an object’s state. It prevents objects from being left invalid, although mutation may violate the condition briefly. section 6.3.4
Apply the principle by:
- Expressing a condition over the class’s member variables. section 6.3.4
- Checking it before a constructor or state-changing member function returns. section 6.3.4
- Using preconditions and postconditions alongside the invariant to define permitted calls and expected results. section 6.3
CircularBuffer
A circular buffer keeps head and tail within the range 0 through capacity minus 1: (0 <= head < capacity) and (0 <= tail < capacity). Incrementing each index with modulo capacity preserves this condition. Assertions check the invariant after construction and after add() or remove(); an invalid remove() call instead violates its precondition and aborts. section 6.3.1 section 6.3.4
(0 <= head < capacity) and (0 <= tail < capacity)
Inspect the compact invariant expression used for the circular buffer’s index bounds. section 6.3.4
