// Stack<E> is a Java interface type describing an abstract data type of
// immutable stacks of elements of type E.
// 
// To give an algebraic specification of Stack<E>, we'll need a notation
// for producing an empty Stack<E>.  In implementations of Stack<E>,
// there's likely to be a static factory method that returns an empty
// Stack<E>, so we'll assume the following method is available and
// returns an empty Stack<E>:
// 
//     Stack<E> empty ();
//
// Algebraic specification:
//
//     empty().isEmpty()  =  true
//     s.push(x).isEmpty()  =  false
// 
//     s.push(x).top()  =  x
// 
//     s.push(x).pop()  =  s
// 
//     empty().size()  =  0
//     s.push(x).size()  =  1 + s.size()

public interface Stack<E> {

    // Returns a Stack that's just like this one except
    // its top element is x and its pop is this Stack.

    public Stack<E> push (E x);

    // Returns true if and only if this Stack is empty.

    public boolean isEmpty ();

    // Returns the top element of this Stack (which must be non-empty).

    public E top ();

    // Returns the pop of this Stack (which must be non-empty).

    public Stack<E> pop ();

    // Returns the size (number of elements) of this Stack.

    public int size ();
}