package dataStructures;

import java.util.*;

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

public interface Table {

  /**
   * Cria uma Tabela vazia
   * @return uma tabela vazia
   */

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

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

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

  /**
   * Verifica se uma dada chave pertence à tabela
   * @param key A chave a procurar
   * @return TRUE se a chave pertence, FALSE c.c.
   */

  //@ requires key != null;
  //@ ensures \old(isEmpty()) ==> !\result;
  /*@ pure @*/ boolean contains(Object key);

  /**
   * Insere na tabela o item com chave key
   * @param key A chave do elemento
   * @param item A referência para o elemento a inserir
   */

  //@ requires  item != null && key != null;
  //@ requires !contains(key);
  //@ ensures  !isEmpty();
  //@ ensures   contains(key);
  //@ ensures   retrieve(key).equals(item);
  void insert(Object item, Object key);

  /**
   * Devolve o elemento com chave key
   * @param key A chave a procurar
   * @return A referência do objecto com a chave
   */

  //@ requires key != null;
  //@ requires contains(key);
  /*@ pure @*/ Object retrieve(Object key);

  /**
   * Remove o elemento com chave key
   * @param key A chave a procurar
   */

  //@ requires key != null;
  //@ ensures \old(isEmpty()) ==> isEmpty();
  //@ ensures !contains(key);
  void remove(Object key);

  /**
   * A tabela 't' é igual a esta? Duas tabelas são iguais se contiverem
   *  exactamente os mesmos pares (key,item).
   * @param t A tabela a ser comparada
   * @return TRUE se são iguais, FALSE c.c.
   */

  //@ requires t != null;
  /*@ pure @*/ boolean equals(Table t);

  /**
   * @return Um iterator para os elementos do conjunto
   */

  /*@ pure @*/ Iterator iterator();

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

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

} // endInterface Table