top

• Inputs: S (a stack)
• Outputs: E (a stack element)
• Preconditions: S is not empty
• Postconditions: E is the top element on S (S is unchanged)

pop

• Inputs: S (a stack)
• Outputs: S' (i.e. S changed)
• Preconditions: S is not empty
• Postconditions: because S is not empty, it has a top element T and a stack R of remaining elements. S'=R.

push

• Inputs: S (a stack), V (a value)
• Outputs: S' (i.e. S changed)
• Preconditions: V is of appropriate type for an element of S
• Postconditions: S' has V as its top element and S as its remaining elements.