/**
 * Array-based implementation of the stack.
 */
public class Stack
{

    /**
     * Construct the stack.
     */
    public Stack( int capacity )
    {
        theArray = new Object[ capacity ];
        topOfStack = -1;
	//@ set theArray.owner = this;
    }

    /**
     * Test if the stack is logically empty.
     */
    /*@ pure */
    public boolean isEmpty( )
    {
        return topOfStack == -1;
    }

    /**
     * Test if the stack is logically full.
     */
    /*@ pure */
    public boolean isFull( )
    {
        return topOfStack == theArray.length;
    }

    /**
     * Get the most recently inserted item in the stack.
     * Does not alter the stack.
     */
    /*@ pure */
    public Object top( )
    {
        if( isEmpty( ) )
            return null;
        return theArray[ topOfStack ];
    }

    /**
     * Remove the most recently inserted item from the stack.
     */
    /*@ modifies this.topOfStack, this.theArray[*]; */
    public void pop( )
    {
        theArray[ topOfStack-- ] = null;
    }

    /**
     * Insert a new item into the stack, if not already full.
     */
    /*@ modifies this.topOfStack, this.theArray[*]; */
    public void push( Object x )
    {
        theArray[ topOfStack++ ] = x;
    }


    /*@ invariant \typeof(this.theArray) == \type(java.lang.Object[]); */
    /*@ invariant theArray.owner == this; */
    /* spec_public */ private Object [ ] theArray;

    /* spec_public */ private int        topOfStack;
}