previous | start | next

## Class Invariants

- Example: Circular array queue

      0 <= head && head < elements.length

- First check it's true for constructor
- - Sets `head = 0`
  - Need precondition `size > 0`!
- Check mutators. Start with `add`
- - Sets `headnew = (headold + 1) % elements.length`
  - We know `headold` > 0 (Why?)
  - `%` operator property:

        0 <= headnew && headnew < elements.length

- What's the use? Array accesses are correct!

      return elements[head];

previous | start | next