Collection: elements of some proper type T
Operations:

  • void push (T t)
  • void pop ()
  • T top ()
  • bool empty ()
  • unsigned int size ()
  • constructor and destructor

Axioms: (for any stack S)

  1. S.size(), S.empty(), S.push(t) are always defined
  2. S.pop() and S.top() are defined iff S.empty() is false
  3. S.empty(), S.size(), S.top() do not change S
  4. S.empty() is true iff 0 = S.size()
  5. S.push(t) followed by S.pop() leaves S unchanged
  6. after S.push(t), S.top() returns t
  7. S.push(t) increases S.size() by 1
  8. S.pop() decreases S.size() by 1