SE450: Horstmann Chapter 3: 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 remove
- Sets head_new = (head_old + 1) % elements.length
- We know head_old >= 0 (Why?)
- % operator property:
```
0 <= head_new && head_new < elements.length
```
What's the use? Array accesses are correct!
```
return elements[head];
```