// DO NOT EDIT THIS FILE
// Only edit Stack.java

/**
 * StackCheck is a class which calls Stack and verifies that the
 * written specification is sufficient.
 **/
public class StackCheck
{

  /**
   * 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() {
    Stack s;
    s = new Stack(1);
    s.push(element());
    s = new Stack(2);
    s.push(element());
    s.push(element());
  }

  /**
   * Check that the isEmpty specification is correctly related to the
   * push specification.
   **/
  public static void checkIsEmpty() {
    Stack s = new Stack(2);

	// new stack should be empty
    //@ assert s.isEmpty();
    
    s.push(element());
	// 1-elt stack should not be empty
    //@ assert !s.isEmpty();

    s.push(element());
	// 2-elt stack should not be empty
    //@ assert !s.isEmpty();
  }

  /**
   * Check that the isFull specification is correctly related to the
   * push specification.
   **/
  public static void checkIsFull() {
    Stack s = new Stack(2);
    
	// new stack should not be full
    //@ assert !s.isFull();
    
    s.push(element());
	// 1-elt stack should not be full
    //@ assert !s.isFull();
    
    s.push(element());
	// 2-elt stack should be full
    //@ assert s.isFull();
  }

  /**
   * Check that top returns null iff the queue is empty.
   **/
  public static void checkTop() {
    Stack s = new Stack(2);
    
	// Top of new stack should be null
    //@ assert s.top() == null;
    
    s.push(element());
	// Top of 1-elt stack should be non-null
    //@ assert s.top() != null;

  }

  /**
   * Check that legal call sequences to the constructor, push, and pop
   * throw no runtime exceptions.
   **/
  public static void checkPop() {
    Stack s = new Stack(2);
    
    s.push(element());
    s.pop();
    
    s.push(element());
    s.push(element());
    s.pop();
    s.pop();
  }

}