public interface Queue {
  //@ public model instance JMLObjectBag elements;

  /*@
    @ public normal_behavior
    @   requires ! isEmpty();
    @   ensures elements.has(\result);
    @
    @ also
    @
    @ public exceptional_behavior
    @   signals(EmptyQueueException) isEmpty()
    @*/
  /*@ pure @*/ Object peek() throws EmptyQueueException;

  /*@
    @ public normal_behavior
    @   assignable elements
    @   requires !isEmpty();
    @   ensures elements.equals(((JMLObjectBag)\old(elements)).remove(\result)) &&
    @           \result.equals(\old(peek())) &&
    @           size()==\old(size())-1
    @
    @ also
    @
    @ public exceptional_behavior
    @   signals(EmptyQueueException) isEmpty()
    @*/
  Object dequeue() throws EmptyQueueException;

  /*@
    @   assignable elements
    @   ensures elements.equals(((JMLObjectBag)\old(elements)).add(item)) &&
    @           size()==\old(size())+1
    @*/
  void enqueue(Object item);

  /*@
    @   ensures \result==elements.isEmpty() &&
    @           size()>0  => !isEmpty() &&
    @           size()==0 => isEmpty()
    @*/
  /*@ pure @*/ boolean isEmpty();

  /*@
    @   ensures \result==elements.size() &&
    @           isEmpty()  => size()==0 &&
    @           !isEmpty() => size()>0
    @*/
  /*@ pure @*/ int size();
}

class EmptyQueueException extends Exception {}