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