package dataStructures;

import java.util.*;

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

 public interface Set {

   /**
    * Criar um conjunto vazio
    * @return um conjunto vazio
    */

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

   /**
    * O conjunto está vazio?
    * @return TRUE se a estrutura está vazia, FALSE c.c.
    */

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

   /**
    * Devolver a cardinalidade do conjunto
    * @return o número de elementos no conjunto
    */

   //@ ensures  isEmpty() ==> \result == 0;
   //@ ensures !isEmpty() ==> \result >  0;
   /*@ pure @*/ int length();

   /**
    * O objecto item pertence ao conjunto?
    * @param item A referência do elemento a procurar
    * @return TRUE se o elemento existe no conjunto, FALSE c.c.
    */

   //@ requires item != null;
   /*@ pure @*/ boolean belongs(Object item);

   /**
    * Inserir o item no conjunto
    * @param item A referência do elemento a inserir no conjunto
    */

   //@ requires item != null;
   //@ ensures belongs(item);
   //@ ensures  \old(belongs(item)) ==> equals((Set)(\old(clone())));
   //@ ensures !\old(belongs(item)) ==> length() == \old(length()) + 1;
   void insert(Object item);

   /**
    * Remover o item do conjunto
    * @param item A referência do elemento a remover do conjunto
    */

   //@ requires item != null;
   //@ ensures  \old(belongs(item)) ==> !belongs(item);
   //@ ensures !\old(belongs(item)) ==> equals((Set)(\old(clone())));
   void remove(Object item);

   /**
    * Inserir os elementos do conjunto 's'
    * @param s A referência do conjunto a unir
    */

   //@ requires s != null;

   // ?JML? ensures (\forall Object item; s.belongs(item); belongs(item));
   // ou:
   /*@ public pure model boolean haveAll(Set s) {
     @   for (Iterator item = s.iterator(); item.hasNext(); )
     @     if (!belongs(item.next()))
     @       return false;
     @   return true;
     @ }
     @ ensures haveAll(s);
     @*/
   void union(Set s);

   /**
    * Remover os elementos que não pertencem a 's'
    * @param s A referência do conjunto a intersectar
    */

   //@ requires s != null;
   void intersection(Set s);

   /**
    * Remover os elementos que pertencem a 's'
    * @param s A referência do conjunto a subtrair
    */

   //@ requires s != null;
   void subtraction(Set s);

   /**
    * Este conjunto contém 's'?
    * @param s O conjunto que está ou não contido
    * @return TRUE se 'this' contem 's', FALSE c.c.
    */

   //@ requires s != null;
   /*@ pure @*/ boolean contains(Set s);

   /**
    * É este conjunto igual a 's'?
    * @param s O conjunto a ser comparado
    * @return TRUE se são iguais, FALSE c.c.
    */

   //@ requires s != null;
   //@ ensures \result == contains(s) && s.contains(this);
   /*@ pure @*/ boolean equals(Set s);

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

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

   /**
    * Criar uma copia da estrutura.
    * @return devolve uma referencia para a cópia
    */

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

}  // endInterface Set