package dataStructures;

/**
 * <p>Titulo: A interface do TDA Fila</p>
 * <p>Descrição: O desenho da Fila (Queue) com os respectivos contratos JML</p>
 * @version 1.0
 */

 public interface Queue {

   //@ public invariant !isEmpty() ==> front() != null;

   /**
    * Criar uma Fila vazia
    * @return uma fila vazia
    */

   //@ ensures \result.isEmpty();
   /*@ pure @*/ Queue empty();

   /**
    * A Fila está vazia?
    * @return devolve TRUE se a estrutura está vazia, FALSE c.c.
    */

   /*@ pure @*/ boolean isEmpty();

   /**
    * Inserir um elemento no fim da Fila
    * @param item A referência do elemento a inserir no fim da Fila
    */

   //@ requires item != null;
   //@ requires !isEmpty() ==> item.getClass() == front().getClass();
   //@ ensures  !isEmpty();
   //@ ensures  \old(isEmpty())    ==> front().equals(item);
   //@ ensures  !(\old(isEmpty())) ==> front().equals(\old(front()));
   void enqueue(Object item);

   /**
    * Devolver o primeiro elemento da Fila
    * @return devolve uma referência do elemento na frente da Fila
    */

   //@ requires  !isEmpty();
   /*@ pure @*/ Object front();

   /**
    * Remover o primeiro elemento da Fila
    */

   //@ requires  !isEmpty();
   /*@ ensures (*
     @  dequeue(enqueue(Q,I)) =
     @  if isEmpty(Q) then empty else enqueue(dequeue(Q),I) *);
     @*/
   void dequeue();

   /**
    * É a Fila 'q' igual a esta?
    * @param q A fila a ser comparada
    * @return devolve TRUE se q==this, FALSE c.c.
    */

   //@ requires q != null;
   /*@ pure @*/ boolean equals(Queue q);

   /**
    * Devolver uma cópia da estrutura.
    * @return devolve uma referência para a cópia
    */

   //@ also
   //@ ensures (\result != this) && equals((Queue)\result);
   /*@ pure @*/ Object clone();

}  // endInterface Queue