/**
 * StackArCheck is a class which calls StackAr and verifies that the
 * written specification is sufficient.
 **/
public class StackArCheck
{
    
    /**
     * Helper method to generate elements to place in the queue.
     * Stack elements are never null.
     **/
    private static Object element()
    //@ ensures \result != null;
    {
        return new Object();
    }
    
    /**
     * Check that legal call sequences to the constructor and push throw
     * no runtime exceptions.
     **/
    public static void checkConstructor() {
        StackAr s;
        s = new StackAr(1);
        s.push(element());
        s = new StackAr(2);
        s.push(element());
        s.push(element());
    }
    
    /**
     * Check that the isEmpty specification is correctly related to the
     * push specification.
     **/
    public static void checkIsEmpty() {
        StackAr s = new StackAr(2);
        
        if (! s.isEmpty())
            throw new RuntimeException("New stack should be empty");
        
        s.push(element());
        if (s.isEmpty())
            throw new RuntimeException("1-elt stack should not be empty");
        
        s.push(element());
        if (s.isEmpty())
            throw new RuntimeException("2-elt stack should not be empty");
    }
    
    /**
     * Check that the isFull specification is correctly related to the
     * enqueue specification.
     **/
    public static void checkIsFull() {
        StackAr s = new StackAr(2);
        
        if (s.isFull())
            throw new RuntimeException("New stack should not be full");
        
        s.push(element());
        if (s.isFull())
            throw new RuntimeException("1-elt stack should not be full");
        
        s.push(element());
        if (! s.isFull())
            throw new RuntimeException("2-elt stack should be full");
    }
    
    /**
     * Check that the makeEmpty specification is correctly related the
     * the isEmpty specifiation.
     **/
    public static void checkMakeEmpty() {
        StackAr s = new StackAr(2);
        
        s.push(element());
        s.makeEmpty();
        if (! s.isEmpty())
            throw new RuntimeException("Emptied stack should be empty");
    }
    
    /**
     * Check that top returns null iff the queue is empty.
     **/
    public static void checkTop() {
        StackAr s = new StackAr(2);
        
        if (s.top() != null)
            throw new RuntimeException("Top of new stack should be null");
        
        s.push(element());
        if (s.top() == null)
            throw new RuntimeException("Top of 1-elt stack should be non-null");
    }
    
    /**
     * Check that legal call sequences to the constructor, push, and pop
     * throw no runtime exceptions.
     **/
    public static void checkPop() {
        StackAr s = new StackAr(2);
        
        s.push(element());
        s.pop();
        
        s.push(element());
        s.push(element());
        s.pop();
        s.pop();
    }
    
    /**
     * Check that topAndPop returns null iff the stack is empty.
     **/
    public static void checkTopAndPop() {
        StackAr s = new StackAr(2);
        
        if (s.topAndPop() != null)
            throw new RuntimeException("Pop of new stack should be null");
        
        s.push(element());
        if (s.topAndPop() == null)
            throw new RuntimeException("Pop of 1-elt stack should be non-null");
        if (s.topAndPop() != null)
            throw new RuntimeException("Second pop of 1-elt stack should be null");
        
        s.push(element());
        s.push(element());
        if (s.topAndPop() == null)
            throw new RuntimeException("Pop of 2-elt stack should be non-null");
        if (s.topAndPop() == null)
            throw new RuntimeException("Second pop of 2-elt stack should be non-null");
        if (s.topAndPop() != null)
            throw new RuntimeException("Third pop of 2-elt stack should be null");
    }
    
}