UNC-CH COMP 410
ADT Axiomatic Semantics
STACK of E (LIFO list)
STACK is the type we are defining
The list/stack contains elements of some type E
signatures (operations and types of parameters/return value)
new: --> STACK (canonical constructor)
push: STACK x E --> STACK (canonical constructor)
pop: STACK --> STACK
top: STACK --> E
size: STACK --> nat (naturals, int >=0 )
empty: STACK --> boolean
axioms (behavior)
size(new) = 0
size(push(S,e)) = size(S) + 1
empty(new) = true
empty(push(S,e)) = false
top(new) = error
top(push(S,e)) = e
pop(new) = new
pop(push(S,e)) = S