The Invariant of the Bag ADT
We write an explicit statement of how the data structure we chose to represent the bag is going to be used.
This is called the invariant of the ADT.
The invariant is an implicit part of the postcondition of each member function.