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

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

  /**
   * Helper method to generate elements to place in the queue.
   * Queue elements are never null.
   **/
  private static Object element()
  //@ ensures \result != null;
  {
    return new Object();
  }

  /**
   * Check that legal call sequences to the constructor and enqueue
   * throw no runtime exceptions.
   **/
  public static void checkConstructor() {
    QueueAr q;
    q = new QueueAr(1);
    q.enqueue(element());
    q = new QueueAr(2);
    q.enqueue(element());
    q.enqueue(element());
  }

  /**
   * Check that the isEmpty specification is correctly related to the
   * enqueue specification.
   **/
  public static void checkIsEmpty() {
    QueueAr q = new QueueAr(2);

    if (! q.isEmpty())
      throw new RuntimeException("New queue should be empty");

    q.enqueue(element());
    if (q.isEmpty())
      throw new RuntimeException("1-elt queue should not be empty");

    q.enqueue(element());
    if (q.isEmpty())
      throw new RuntimeException("2-elt queue should not be empty");
  }

  /**
   * Check that the isFull specification is correctly related to the
   * enqueue specification.
   **/
  public static void checkIsFull() {
    QueueAr q = new QueueAr(2);

    if (q.isFull())
      throw new RuntimeException("New queue should not be full");

    q.enqueue(element());
    if (q.isFull())
      throw new RuntimeException("1-elt queue should not be full");

    q.enqueue(element());
    if (! q.isFull())
      throw new RuntimeException("2-elt queue should be full");
  }

  /**
   * Check that the makeEmpty specification is correctly related the
   * the isEmpty specifiation.
   **/
  public static void checkMakeEmpty() {
    QueueAr q = new QueueAr(2);

    q.enqueue(element());
    q.makeEmpty();
    if (! q.isEmpty())
      throw new RuntimeException("Emptied queue should be empty");
  }

  /**
   * Check that getFront returns null iff the queue is empty.
   **/
  public static void checkGetFront() {
    QueueAr q = new QueueAr(2);

    if (q.getFront() != null)
      throw new RuntimeException("Front of new queue should be null");

    q.enqueue(element());
    if (q.getFront() == null)
      throw new RuntimeException("Front of 1-elt queue should be non-null");
  }

  /**
   * Check that dequeue returns null iff the queue is empty.
   **/
  public static void checkDequeue() {
    QueueAr q = new QueueAr(2);

    if (q.dequeue() != null)
      throw new RuntimeException("Dequeue of new queue should be null");

    q.enqueue(element());
    if (q.dequeue() == null)
      throw new RuntimeException("Dequeue of 1-elt queue should be non-null");
    if (q.dequeue() != null)
      throw new RuntimeException("Second dequeue of 1-elt queue should be null");
    
    q.enqueue(element());
    q.enqueue(element());
    if (q.dequeue() == null)
      throw new RuntimeException("Dequeue of 2-elt queue should be non-null");
    if (q.dequeue() == null)
      throw new RuntimeException("Second dequeue of 2-elt queue should be non-null");
    if (q.dequeue() != null)
      throw new RuntimeException("Third dequeue of 2-elt queue should be null");
  }

}