Invariant Documentation
The invariant of an ADT is placed in the implementation file of its class.
The implementor of the class must insure that the invariant holds after each of the member functions returns. He or she may assume that the invariant holds before each of the member functions is activated, except for the constructor.