package dataStructures;

import java.util.*;

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

public interface BinTree {

  // Não é possível ter objectos nulos numa árvore não vazia
  //@ public invariant !isEmpty() ==> root() != null;

  /**
   * Cria uma Árvore vazia
   * @return uma árvore vazia
   */

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

  /**
   * Devolve true se a árvore está vazia, senão false
   * @return Devolve TRUE se a estrutura está vezia, FALSE c.c.
   */

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

  /**
   * Constrói uma árvore
   * @param item A referência do objecto a ser guardado
   * @param left A referência da árvore da esquerda
   * @param right A referência da árvore da direita
   */

  //@ requires right != null && !right.isEmpty() ==> item.getClass() == right.root().getClass();
  //@ requires left != null && !left.isEmpty() ==> item.getClass() ==  left.root().getClass();
  //@ ensures item != null ==> !isEmpty();
  //@ ensures item != null ==> root().equals(item);
  //@ ensures item != null ==> left().equals(left);
  //@ ensures item != null ==> right().equals(right);
  void constr(Object item, BinTree left, BinTree right);

  /**
   * Devolve a informação da raiz da árvore
   * @return A referência do objecto que está na raiz
   */

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

  /**
   * Devolve a árvore da esquerda
   * @return A referência da subárvore da esquerda
   */

  //@ requires !isEmpty();
  /*@ pure @*/ BinTree left();

  /**
   * Devolve a árvore da direita
   * @return A referência da subárvore da direita
   */

  //@ requires !isEmpty();
  /*@ pure @*/ BinTree right();

  /**
   * Devolve o número de elementos da Árvore
   * @return O número de elementos da Árvore
   */

  //@ ensures  isEmpty() ==> \result == 0;
  //@ ensures !isEmpty() ==> \result == 1 + left().length() + right().length();
  /*@ pure @*/ int length();

  /**
   * Devolve a altura da Árvore (i.e., a dimensão do maior caminho)
   * @return A altura da árvore
   */

  //@ ensures  isEmpty() ==> \result == 0;
  //@ ensures !isEmpty() ==> \result == 1 + Math.max(left().height(), right().height());
  /*@ pure @*/ int height();

  /**
   * Verifica se é uma folha
   * @return TRUE se é uma folha, FALSE c.c.
   */

  //@ ensures \result == (!isEmpty() && left().isEmpty() && right().isEmpty());
  /*@ pure @*/ boolean isLeaf();

  /**
   * Verifica se duas Árvores são iguais
   * @param t A árvore para ser comparada
   * @return TRUE se as duas árvores são iguais (têm a mesma estrutura e
            e guardam a mesma informação)
   */

  //@ requires t != null;
  //@ ensures isEmpty() ==> t.isEmpty();
  //@ ensures t.isEmpty() ==> isEmpty();
  //@ ensures !isEmpty() && !t.isEmpty() ==> \result == (root().equals(t.root()) && left().equals(t.left()) && right().equals(t.right()));
  /*@ pure @*/ boolean equals(BinTree t);

  /**
   * Atravessa a árvore de forma prefixa
   * @param op O operador a ser executado em cada nó
   */

  //@ requires op != null;
  void prefix(Visitor op);

  /**
   * Atravessa a árvore de forma infixa
   * @param op O operador a ser executado em cada nó
   */

  //@ requires op != null;
  void infix(Visitor op);

  /**
   * Atravessa a árvore de forma sufixa
   * @param op O operador a ser executado em cada nó
   */

  //@ requires op != null;
  void sufix(Visitor op);

  /**
   * @return Um iterator para os elementos do conjunto (travessia por largura)
   */
  Iterator iterator();

  /**
   * Devolve uma copia da estrutura da Árvore. Nao copia os conteudos!
   * @return devolve uma referencia para a cópia
   */
  //@ also
  //@ ensures (\result != this) && equals((BinTree)\result);
  /*@ pure @*/ Object clone();

}  // endInterface BinTree