Algebraic Specifications for STACK

Next
    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