| Next |
pop(new()) = new()
pop(push(S,i)) = S
new: --> STACK (operations)
push: STACK x INT --> STACK
pop: STACK --> STACK
top: STACK --> INT U { error }
empty: STACK --> BOOLEAN