11.5: Stack Example (1)
Class methods implement an abstract specification of a useful task.
The features of generic class Stack[G] are:
- count, empty, full, put, remove, item;
The specification of each feature includes
- require <pre-condition> ;
- ensure <post-condition> ;
- invariant <loop-invariant>
- implementation;
- [side effects if pre-conditions not met? - RJL].