****************************************************************

Example: an immutable ADT, Stack (of int)

    empty:                 -->  Stack
    push:     Stack x int  -->  Stack
    isEmpty:  Stack        -->  boolean
    top:      Stack        -->  int
    pop:      Stack        -->  Stack

    isEmpty (empty())  =  true
    isEmpty (push (s, n))  =  false

    top (push (s, n))  =  n

    pop (push (s, n))  =  s

Note:  This specification does not define pop and top on an
empty stack.

****************************************************************

public abstract class Stack {

    // The basic creators are empty and push.

    // Returns an empty stack.

    public static Stack empty () {
        return new Empty();
    }

    // Returns a stack representing n pushed onto s.

    public static Stack push (Stack s, int n) {
        return new Push (s, n);
    }

    // Other public methods.

    // Returns true iff the given stack is empty.

    public static boolean isEmpty (Stack s) {
        return s.isEmpty1();
    }

    // Returns the top element of the given stack, which must be nonempty.

    public static int top (Stack s) {
        return s.top1();
    }

    // Returns the pop of the given stack, which must be nonempty.

    public static Stack pop (Stack s) {
        return s.pop1();
    }

    // Abstract methods for the accessors.

    // Returns true iff this stack is empty.

    abstract boolean isEmpty1 ();

    // Returns the top element of this stack, which must be nonempty.

    abstract int top1 ();

    // Returns the other elements of this stack, which must be nonempty.

    abstract Stack pop1 ();

}

// The class of objects created by empty().

class EmptyStack extends Stack {

    // Initializes this empty stack.

    EmptyStack () { }

    boolean isEmpty1 () { return true; }

    int top1 () {
        throw new IllegalArgumentException (msgTop);
    }

    Stack pop1 () {
        throw new IllegalArgumentException (msgPop);
    }

    private static final String msgTop
        = "Can't take the top of an empty stack.";

    private static final String msgPop
        = "Can't pop an empty stack.";

}

// The class of objects created by push(s,n).

class PushStack extends Stack {

    private Stack s;                 // the pop of this Stack
    private int n;                   // the top of this Stack

    // Initializes this stack with top n and pop s.

    PushStack (Stack s, int n) {
        this.s = s;
        this.n = n;
    }

    boolean isEmpty1 () { return false; }

    int top1 () {
        return n;
    }

    Stack pop1 () {
        return s;
    }

}