/**
 * Array-based implementation of the stack.
 * @author Mark Allen Weiss
 **/
public class StackAr
{
    
    /*@ spec_public */ private Object [ ] theArray;
    /*@ invariant theArray.owner == this; */
    /*@ invariant \typeof(theArray) == \type(java.lang.Object[]); */
    /*@ spec_public */ private int        topOfStack;
    
    /**
     * Construct the stack.
     * @param capacity the capacity.
     **/
    public StackAr( int capacity )
    {
        theArray = new Object[ capacity ];
        /*@ set theArray.owner = this; */
        topOfStack = -1;
    }
    
    /**
     * Test if the stack is logically empty.
     * @return true if empty, false otherwise.
     **/
    public boolean isEmpty( )
    {
        return topOfStack == -1;
    }
    
    /**
     * Test if the stack is logically full.
     * @return true if full, false otherwise.
     **/
    public boolean isFull( )
    {
        return topOfStack == theArray.length - 1;
    }
    
    
    /**
     * Make the stack logically empty.
     **/
    public void makeEmpty( )
    {
        for (int i = 0; i < topOfStack + 1; i++){
            theArray[i] = null;
        }
        topOfStack = -1;
    }
    
    /**
     * Get the most recently inserted item in the stack.
     * Does not alter the stack.
     * @return the most recently inserted item in the stack, or null, if empty.
     **/
    public Object top( )
    {
        if( isEmpty( ) )
            return null;
        return theArray[ topOfStack ];
    }
    
    /**
     * Remove the most recently inserted item from the stack.
     * @exception RuntimeException if stack is already empty.
     **/
    public void pop( ) throws RuntimeException
    {
        if( isEmpty( ) )
            throw new RuntimeException( "Underflow" );
        theArray[ topOfStack-- ] = null;
    }
    
    /**
     * Insert a new item into the stack, if not already full.
     * @param x the item to insert.
     * @exception RuntimeException if stack is already full.
     **/
    public void push( Object x ) throws RuntimeException
    {
        if( isFull( ) )
            throw new RuntimeException( "Overflow" );
        theArray[ ++topOfStack ] = x;
    }
    
    /**
     * Return and remove most recently inserted item from the stack.
     * @return most recently inserted item, or null, if stack is empty.
     **/
    public Object topAndPop( )
    {
        if( isEmpty( ) )
            return null;
        Object topItem = top( );
        theArray[ topOfStack-- ] = null;
        return topItem;
    }
    
}