class Queue
{
  private int[] a;
  private int head = 0;
  private int tail = 0;
  private int count = 0;
  private int N = 3;

  //@ invariant a != null && a.length > 0;

  //@ invariant 0 <= head && head < a.length;
  //@ invariant 0 <= tail && tail < a.length;
  //@ invariant 0 <= count && count <= a.length;

  //@ invariant (head <  tail ==> count == tail-head);
  //@ invariant (head >  tail ==> count == a.length-(head-tail));
  //@ invariant (head == tail ==> (count == 0 || count == a.length));

  /*@ private normal_behavior
    @ assignable a;
    @ ensures a != null && a.length == N;
    @ ensures head == 0 && tail == 0 && count == 0; 
    @*/
  public Queue()
  {
    a = new int[N];
  }

  /*@ private normal_behavior
    @ assignable \nothing;
    @ ensures \result == (count == 0); 
    @*/
  public boolean isempty()
  {
    return count == 0;
  }

  /*@ private normal_behavior
    @ assignable a, a[*], head, tail, count;
    @ ensures count == \old(count)+1;
    @ ensures \old(count) < \old(a).length ==>
    @   a == \old(a) &&
    @   (\forall int i; 0 <= i && i < a.length && i != \old(tail); 
    @      a[i] == \old(a[i])) && 
    @   a[\old(tail)] == value &&
    @   head == \old(head) &&
    @   (\old(tail) <  a.length-1 ==> tail == \old(tail)+1) &&
    @   (\old(tail) == a.length-1 ==> tail == 0);
    @ ensures \old(count) == \old(a).length ==>
    @   a.length > \old(a).length &&
    @   a[\old(count)] == value &&
    @   (\forall int i; 0 <= i && i < \old(count);
    @     (i <  \old(a.length-head) ==> a[i] == \old(a[i+head])) &&
    @     (i >= \old(a.length-head) ==> a[i] == \old(a[i-a.length+head]))) &&
    @   head == 0 &&
    @   (\old(a.length) <  a.length-1 ==> tail == \old(count)+1) &&
    @   (\old(a).length == a.length-1 ==> tail == 0);
    @*/
  public void enqueue(int value)
  {
   if (count == a.length) resize();
   count = count+1;
   a[tail] = value;
   tail = tail+1;
   if (tail == a.length) tail = 0;
  }

  /*@ private normal_behavior
    @ requires count > 0;
    @ assignable count, head;
    @ ensures count == \old(count)-1;
    @ ensures \old(head) <  a.length-1 ==> head == \old(head)+1; 
    @ ensures \old(head) == a.length-1 ==> head == 0; 
    @*/
  public void dequeue()
  {
    count = count-1;
    head = head+1;
    if (head == a.length) head = 0;
  }

  /*@ private normal_behavior
    @ requires count > 0;
    @ assignable \nothing;
    @ ensures \result == a[head]; 
    @*/
  public int first()
  {
    return a[head];
  }

  /*@ private normal_behavior
    @ assignable a, head, tail;
    @ ensures \fresh(a) && a.length > \old(a).length;
    @ ensures head == 0 && tail == count;
    @ ensures (\forall int i; 0 <= i && i < \old(a.length);
    @       (i <  \old(a.length-head) ==> a[i] == \old(a[i+head])) &&
    @       (i >= \old(a.length-head) ==> a[i] == \old(a[i-a.length+head])));
    @*/
  private void resize()
  {
    int b[] = new int[2*a.length+1];
    for (int i=head; i<a.length; i++)
      b[i-head] = a[i];
    for (int i=0; i<head; i++)
      b[i+a.length-head] = a[i];
    head = 0;
    tail = count;
    a = b;
  }
}