public /*@  pure @*/ class QueueModel
{
/*@   // the queue with e added to the tail of this queue
  @   public model QueueModel enqueue(int e);
  @
  @   // the element at the front of the queue
  @   public model int head();
  @
  @   // the queue with the head removed from this queue
  @   public model QueueModel dequeue();
  @
  @   // the number of elements in the queue
  @   public model int length();
  @
  @   // the element at position i in this queue (0 = head)
  @   public model int elementAt(int i);
  @
  @   axiom 
  @     (\forall QueueModel q, q2; q != null && q2 != null;
  @       (\forall int e, e2, i; ;
  @
  @         // the constructors
  @         !new QueueModel().equals(q.enqueue(e)) &&
  @         (q.enqueue(e).equals(q2.enqueue(e2)) ==> 
  @            q.equals(q2) && e == e2) &&
  @
  @         // the selectors
  @         q.enqueue(e).head() ==
  @            (q.equals(new QueueModel()) ? e : q.head()) &&
  @         q.enqueue(e).dequeue() ==
  @            (q.equals(new QueueModel()) ? q : (q.dequeue()).enqueue(e)) &&
  @
  @         // convenience operations
  @         q.length() ==
  @           (q.equals(new QueueModel()) ? 0 : 1+q.dequeue().length()) &&
  @         (0 <= i && i <= q.length() ==>
  @           q.enqueue(e).elementAt(i) ==
  @             (i == q.length() ? e : q.elementAt(i)))
  @
  @     ));
  @*/
}