Algebraic Specifications for STACK

    pop(new()) = new()
    pop(push(S,i)) = S

    top(new()) = error
    top(push(S,i)) = i

    empty(new()) = true
    empty(push(S,i)) = false


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

Comments on Axioms

• no implementation implied here

• cannot get a feel for, say, how "push" affects a stack by examining one, or a few, axioms.

  In operational specs, you can.