package dataStructures;

/**
 * <p>Titulo: A interface do TDA Árvore Binária de Pesquisa</p>
 * <p>Descrição: O desenho (SearchBinTree) com os respectivos contratos</p>
 * @version 1.0
 */

public interface SearchBinTree extends BinTree {

 /**
  * @param t Is 't' a searchable tree?
  * @return TRUE se a árvore pode ser pesquisada, FALSE c.c.
  */

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

 /**
  * @param o O objecto a ser procurado
  * @return TRUE se o objecto encontra-se na árvore, FALSE c.c.
  */

 //@ requires o != null;
 //@ requires isSearchable(this);
 //@ ensures  isSearchable(this);
 //@ ensures  isEmpty() ==> !\result;
 /*@ ensures !isEmpty() ==> \result == (o.equals(root()) ||
   @            (o.compareTo(root())<0 && ((SearchBinTree)left()).occurs(o)) ||
   @            (o.compareTo(root())>0 && ((SearchBinTree)right()).occurs(o)));
   @*/
 /*@ pure @*/ boolean occurs(Comparable o);

 /**
  * @param o O objecto a ser inserido
  */

 //@ requires o != null;
 //@ requires !isEmpty() ==> o.getClass() == root().getClass();
 //@ requires isSearchable(this);
 //@ ensures  isSearchable(this);
 //@ ensures  occurs(o);
 //@ ensures  length() == \old(length()) + 1;
 void insert(Comparable o);

 /**
  * @param o O objecto a ser removido
  */

 //@ requires o != null;
 //@ requires isSearchable(this);
 //@ ensures  isSearchable(this);
 //@ ensures  \old(isEmpty()) ==> isEmpty();

 // Por motivo que desconheço, não funcionam...
 // ensures  \old(!isEmpty()) && o.equals(\old(root())) && \old(left().isEmpty()) ==> equals(\old(right()));
 // ensures  \old(!isEmpty()) && o.equals(\old(root())) && \old(right().isEmpty()) ==> equals(\old(left()));
 // Alternativa:
 //@ ensures  \old(!isEmpty()) && o.equals(\old(root())) && \old(left().isEmpty()) ==> (this+"").equals(\old(right()+""));
 //@ ensures  \old(!isEmpty()) && o.equals(\old(root())) && \old(right().isEmpty()) ==> (this+"").equals(\old(left()+""));
 void remove(Comparable o);

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

}  // endInterface SearchBinTree