Sample Contract for Stack::put()
put(x) OBLIGATIONS BENEFITS
Client (Satisfy pre-condition:) (From post-condition:)
(Caller) Only call put (x) on Get stack updated: a non-full stack. not empty; x on top (item yields x); count increased by 1.
Supplier (Satisfy post-condition:) (From precondition:)
(Stack::) Update stack represen- Simpler processing, tation to have x on top thanks to the (item yields x); //and assumption that stack
count increased by 1; //and is not full.