package dataStructures;

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

public interface Heap extends BinTree {

  /**
   * A árvore dada é um amontado (heap)?
   * @param t A árvore em questão
   * @return TRUE se 't' é um amontoado, FALSE c.c.
   */

  //@ requires t != null;
  //@ ensures t.isEmpty() ==> \result;
  /*@ pure @*/ boolean isHeap(BinTree t);

  /**
   * Insere um novo elemento
   * @param o A referência do elemento a ser inserido
   */

  //@ requires o != null;
  //@ requires isHeap(this);
  //@ ensures  isHeap(this);
  //@ ensures  length() == \old(length()) + 1;
  void insert(Comparable o);

  /**
   * Remove o elemento da raiz, e actualiza o amontado
   */

  //@ requires !isEmpty();
  //@ requires isHeap(this);
  //@ ensures  isHeap(this);
  //@ ensures !\old(isEmpty()) ==> length() == \old(length()) - 1;
  void remRoot();

  Object clone(); // JML needs this to work... (?)

}  // endInterface Heap