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