functions
    new : stack;
    push : element * stack  -> stack; 
    empty : stack -> boolean;
    pop : stack -> stack;
    top : stack -> element;
  axioms
    empty( new ) = true
    empty( push(x,s) ) = false
    top( push(x,s) ) = x
    pop( push(x,s) ) = s
  preconditions
    pre: pop( s : stack ) = not empty(s)
    pre: top( s : stack ) = not empty(s)
  end