/**
 *  <p>
 *
 *  Collection non modifiable (immutable) non ordonnée d'éléments non <code>null</code>
 *  ne contenant pas d'éléments dupliqués. Plus formellement, un ensemble ne
 *  contient aucune paire d'éléments <code>e1</code> et <code>e2</code> telle
 *  que <code>e1.equals(e2)</code> . </p> <p>
 *
 *  Cette classe tente de modéliser au mieux le concept mathématique d'ensemble
 *  en définissant les opérations mathématiques usuelles sur les ensembles
 *  (cardinal, union, intersection...). </p>
 *
 * @author     Marc Champesme
 * @version    4 septembre 2005
 * @since      1 septembre 2005
 */

public interface PureEnsemble {
	/*@
	  @ public invariant !contient(null);
	  @ public invariant this.union(this).equals(this);
	  @ public invariant cardinal() >= 0;
	  @*/
	/**
	 *  Renvoie <code>true</code> si cet ensemble contient l'élément spécifié. Plus
	 *  précisément, renvoie <code>true</code> si et seulement si cette liste
	 *  contient un élément <code>e</code> tel que <code>e.equals(elt)</code>.
	 *
	 * @param  elt  L'élément dont on cherche &agrave; savoir s'il appartient
	 *      &agrave; cet ensemble.
	 * @return      <code>true</code> si l'élement spécifié est présent ; <code>false</code>
	 *      sinon.
	 */
	/*@
	  @ old Object[] tabElems = tabElements();
	  @ ensures \result <==> (\exists int i; i >= 0 && i < cardinal();
	  @						tabElems[i].equals(elt));
	  @ pure
	  @*/
	public boolean contient(Object elt);


	/**
	 *  Renvoie <code>true</code> si cet ensemble est inclus dans l'ensemble
	 *  spécifié. Plus précisément, renvoie <code>true</code> si et seulement tout
	 *  élément <code>e</code> de cet ensemble est tel que <code>ens.contient(e)</code>
	 *  .
	 *
	 * @param  ens  L'ensemble dont on souhaite savoir s'il contient cet ensemble.
	 * @return      <code>true</code> si cet ensemble est inclus dans l'ensemble
	 *      spécifié ; <code>false</code> sinon.
	 */
	/*@
	  @ requires ens != null;
	  @ ensures \result <==> this.intersection(ens).equals(this);
	  @ ensures \result ==> cardinal() <= ens.cardinal();
	  @ ensures equals(ens) ==> \result;
	  @
	  @ pure
	  @*/
	public boolean estInclusDans(PureEnsemble ens);


	/**
	 *  Renvoie l'union ensembliste de cet ensemble avec l'ensemble spécifié.
	 *
	 * @param  ens  L'ensemble avec lequel l'union doit etre effectuée.
	 * @return      L'union ensembliste de cet ensemble avec l'ensemble spécifié
	 */
	/*@
	  @ requires ens != null;
	  @ ensures \result != null;
	  @ ensures ens.estInclusDans(\result);
	  @ ensures this.estInclusDans(\result);
	  @ ensures \result.difference(this).estInclusDans(ens);
	  @ ensures \result.difference(ens).estInclusDans(this);
	  @ ensures \result.cardinal() == (this.cardinal() + ens.cardinal()
	  @				   - this.intersection(ens).cardinal());
	  @ pure
	  @*/
	public PureEnsemble union(PureEnsemble ens);


	/**
	 *  Renvoie l'intersection ensembliste de cet ensemble avec l'ensemble
	 *  spécifié.
	 *
	 * @param  ens  L'ensemble avec lequel l'intersection doit etre effectuée.
	 * @return      L'intersection ensembliste de cet ensemble avec l'ensemble
	 *      spécifié
	 */
	/*@
	  @ requires ens != null;
	  @ ensures \result != null;
	  @ ensures \result.estInclusDans(this);
	  @ ensures \result.estInclusDans(ens);
	  @ ensures this.difference(\result).equals(this.difference(ens));
	  @ ensures \result.cardinal() == this.cardinal() - this.difference(ens).cardinal();
	  @ ensures \result.cardinal() == ens.cardinal() - ens.difference(this).cardinal();
	  @ pure
	  @*/
	public PureEnsemble intersection(PureEnsemble ens);


	/**
	 *  Renvoie l'ensemble représentant la différence ensembliste de cet ensemble
	 *  avec l'ensemble spécifié.
	 *
	 * @param  ens  L'ensemble &agrave; soustraire de cet ensemble.
	 * @return      La différence ensembliste de cet ensemble avec l'ensemble
	 *      spécifié
	 */
	/*@
	  @ requires ens != null;
	  @ ensures \result != null;
	  @ ensures \result.estInclusDans(this);
	  @ ensures \result.intersection(ens).estVide();
	  @ ensures \result.union(ens).equals(this.union(ens));
	  @ ensures \result.cardinal() == this.cardinal() - this.intersection(ens).cardinal();
	  @ pure
	  @*/
	public PureEnsemble difference(PureEnsemble ens);



	/**
	 *  Teste si cet ensemble ne contient aucun élément.
	 *
	 * @return    <code>true</code> si cet ensemble ne contient aucun élément ;
	 *      <code>false</code> sinon.
	 */
	/*@
	  @ ensures \result <==> (cardinal() == 0);
	  @ pure
	  @*/
	public boolean estVide();



	/**
	 *  Renvoie le cardinal de cet ensemble.
	 *
	 * @return    le nombre d'éléments de cet ensemble.
	 */
	/*@
	  @ ensures \result >= 0;
	  @ pure
	  @*/
	public int cardinal();


	/**
	 *  Renvoie une nouvelle instance de tableau contenant tous les éléments de cet
	 *  ensemble. L'ordre dans lequel les éléments apparaissent dans le tableau
	 *  n'est pas spécifié: aucune garantie n'est donnée que deux appels successifs
	 *  de cette méthode sur un meme ensemble renvoyent des tableaux dans lesquels
	 *  les éléments sont dans le meme ordre.
	 *
	 * @return    Un tableau contenant tous les éléments de cet ensemble.
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \fresh(\result);
	  @ ensures \result.length == cardinal();
	  @ ensures (\forall int i; i >= 0 && i < \result.length;
	  @						contient(\result[i]));
	  @ ensures (\forall Object o; contient(o);
	  @	  		(\exists int i;i >= 0 && i < \result.length;
	  @	  					\result[i].equals(o)));
	  @ ensures (\forall int i, j; 0 <= i && i < j && j < \result.length;
	  @				!\result[i].equals(\result[j]));
	  @ pure
	  @*/
	public Object[] tabElements();


	/**
	 *  Renvoie un itérateur sur les éléments de cet ensemble. Aucune garantie
	 *  n'est donnée sur l'ordre dans lequel cet itérateur renvoie les éléments.
	 *
	 * @return    Un itérateur sur les éléments de cet ensemble
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.elementSuivantExiste() <==> !this.estVide();
	  @*/
	public Iterateur iterateur();


	/**
	 *  Teste l'égalité entre l'objet spécifié et cet ensemble. Renvoie <code>true</code>
	 *  si et seulement si l'objet spécifié est aussi un <code>Ensemble</code>, que
	 *  les deux ensembles ont le m&ecirc;me nombre d'éléments et que les deux
	 *  ensembles contiennent les m&ecirc;mes elements au sens de <i>equals</i> .
	 *
	 * @param  obj  l'objet &agrave; comparer avec cette liste.
	 * @return      <code>true</code> si l'objet spécifié est composé d'éléments
	 *      <i>equals</i> &agrave; ceux de cette liste ; <code>false</code> sinon
	 */
	/*@
	  @ also
	  @ ensures !(obj instanceof PureEnsemble) ==> !\result;
	  @ ensures obj instanceof PureEnsemble
	  @		==> (\result
	  @			<==> (((PureEnsemble) obj).estInclusDans(this)
	  @			      && estInclusDans((PureEnsemble) obj)));
	  @ ensures \result ==> cardinal() == ((PureEnsemble)obj).cardinal();
	  @ ensures (cardinal() != ((PureEnsemble)obj).cardinal()) ==> !\result;
	  @ ensures \result ==> (hashCode() == ((PureEnsemble)obj).hashCode());
	  @ pure
	  @*/
	public boolean equals(Object obj);


	/**
	 *  Renvoie la valeur du code de hashage de cet ensemble. Le code de hashage
	 *  d'un ensemble est définit comme étant la somme des codes de hashage de ses
	 *  éléments. Ce calcul assure que <code>ens1.equals(ens2)</code> implique que
	 *  <code>ens1.hashCode()==ens2.hashCode()</code> pour toute paire d'ensembles,
	 *  <code>ens1</code> et <code>ens2</code>, comme le spécifie le contrat de
	 *  <code>Object.hashCode</code>.</p>
	 *
	 * @return    la valeur du code de hashage pour cet ensemble.
	 */
	//@ pure
	public int hashCode();

}