public interface Queue {

    //@ public model instance \locset footprint;
    //@ public accessible \inv: footprint;
    //@ public accessible footprint: footprint;  
    
    //@ public instance invariant 0 <= size();
    
    
    /*@ public normal_behaviour
      @   accessible footprint;
      @   ensures \result == size();
      @*/
    public /*@pure@*/ int size(); 
    
    /*@ public normal_behaviour
      @   requires 0 <= index && index < size(); 
      @   accessible footprint;
      @   ensures \result == get(index);
      @
      @ also public exceptional_behaviour
      @   requires index < 0 || size() <= index;
      @   signals_only IndexOutOfBoundsException;
      @*/
    public /*@pure@*/ Object get(int index);
    
    /*@ public normal_behaviour
      @   assignable footprint;
      @   ensures size() == \old(size()) + 1 && get(size() - 1) == o;
      @   ensures (\forall int i; 0 <= i && i < \old(size()); get(i) == \old(get(i)));
      @   ensures \new_elems_fresh(footprint);
      @*/    
     public void enqueue(Object o);
    
    
    /*@ public normal_behaviour
      @   requires size() > 0;
      @   assignable footprint;
      @   ensures \result == \old(get(0));
      @   ensures size() == \old(size()) - 1;
      @   ensures (\forall int i; 0 <= i && i < size(); get(i) == \old(get(i+1)));
      @   ensures \new_elems_fresh(footprint);
      @
      @ also public exceptional_behaviour
      @   requires size() == 0;
      @   assignable \nothing;
      @   signals_only IllegalArgumentException;
      @
      @*/
    public Object dequeue();
}