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