package dataStructures;

/**
 * <p>Titulo: A interface do TDA Pilha</p>
 * <p>Descrição: A interface Pilha (Stack) com os respectivos contratos JML</p>
 * @version 1.0
 */

 public interface Stack {

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

   /**
    * Criar uma Pilha vazia
    * @return uma nova pilha vazia
    */

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

   /**
    * A Pilha está vazia?
    * @return TRUE se está vazia, FALSE c.c.
    */

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

   /**
    * Inserir um elemento no topo da Pilha
    * @param item A referência do elemento a inserir no topo da pilha
    */

   //@ requires item != null;
   //@ requires !isEmpty() ==> item.getClass() == top().getClass();
   //@ ensures top().equals(item);
    void push(Object item);

   /**
    * Devolver o topo da Pilha
    * @return devolve uma referência para o elemento no topo da Pilha
    */

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

   /**
    * Remover o topo da Pilha
    */

   //@ requires !isEmpty();
   //@ ensures (* POP(PUSH(Stack,Item)) = Stack *);
   // ou:
   /*@ public pure model Stack popObservable() {
     @   Stack copy = ((Stack)clone());
     @   copy.pop();
     @   return copy;
     @ }
     @
     @ public pure model Stack pushObservable(Object item) {
     @   Stack copy = ((Stack)clone());
     @   copy.push(item);
     @   return copy;
     @ }
     @ ensures equals(pushObservable(\old(top())).popObservable());
     @*/
   void pop();

   /**
    * A pilha 's' é igual a esta?
    * @param s A pilha a ser comparada
    * @return TRUE se são iguais, FALSE c.c.
    */

   //@ requires s != null;
   /*@ pure @*/ boolean equals(Stack s);

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

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

}  // endInterface Stack