Interface PureEnsemble

All Known Implementing Classes:
TabPureEnsemble

public interface PureEnsemble

Collection non modifiable (immutable) non ordonnée d'éléments non null ne contenant pas d'éléments dupliqués. Plus formellement, un ensemble ne contient aucune paire d'éléments e1 et e2 telle que e1.equals(e2) .

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...).

Since:
1 septembre 2005

Class Specifications
public invariant !this.contient(null);
public invariant this.union(this).equals(this);
public invariant this.cardinal() >= 0;

Specifications inherited from class Object
public represents _getClass <- \typeof(this);

Method Summary
 int cardinal()
          Renvoie le cardinal de cet ensemble.
 boolean contient(java.lang.Object elt)
          Renvoie true si cet ensemble contient l'élément spécifié.
 PureEnsemble difference(PureEnsemble ens)
          Renvoie l'ensemble représentant la différence ensembliste de cet ensemble avec l'ensemble spécifié.
 boolean equals(java.lang.Object obj)
          Teste l'égalité entre l'objet spécifié et cet ensemble.
 boolean estInclusDans(PureEnsemble ens)
          Renvoie true si cet ensemble est inclus dans l'ensemble spécifié.
 boolean estVide()
          Teste si cet ensemble ne contient aucun élément.
 int hashCode()
          Renvoie la valeur du code de hashage de cet ensemble.
 PureEnsemble intersection(PureEnsemble ens)
          Renvoie l'intersection ensembliste de cet ensemble avec l'ensemble spécifié.
 java.lang.Object[] tabElements()
          Renvoie une nouvelle instance de tableau contenant tous les éléments de cet ensemble.
 PureEnsemble union(PureEnsemble ens)
          Renvoie l'union ensembliste de cet ensemble avec l'ensemble spécifié.
 

Method Detail

contient

public boolean contient(java.lang.Object elt)
Renvoie true si cet ensemble contient l'élément spécifié. Plus précisément, renvoie true si et seulement si cette liste contient un élément e tel que e.equals(elt).

Parameters:
elt - L'élément dont on cherche à savoir s'il appartient à cet ensemble.
Returns:
true si l'élement spécifié est présent ; false sinon.
Specifications: pure
old java.lang.Object[] tabElems = this.tabElements();
ensures \result <==> ( \exists int i; i >= 0&&i < this.cardinal(); tabElems[i].equals(elt));

estInclusDans

public boolean estInclusDans(PureEnsemble ens)
Renvoie true si cet ensemble est inclus dans l'ensemble spécifié. Plus précisément, renvoie true si et seulement tout élément e de cet ensemble est tel que ens.contient(e) .

Parameters:
ens - L'ensemble dont on souhaite savoir s'il contient cet ensemble.
Returns:
true si cet ensemble est inclus dans l'ensemble spécifié ; false sinon.
Specifications: pure
requires ens != null;
ensures \result <==> this.intersection(ens).equals(this);
ensures \result ==> this.cardinal() <= ens.cardinal();
ensures this.equals(ens) ==> \result ;

union

public PureEnsemble union(PureEnsemble ens)
Renvoie l'union ensembliste de cet ensemble avec l'ensemble spécifié.

Parameters:
ens - L'ensemble avec lequel l'union doit etre effectuée.
Returns:
L'union ensembliste de cet ensemble avec l'ensemble spécifié
Specifications: pure
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());

intersection

public PureEnsemble intersection(PureEnsemble ens)
Renvoie l'intersection ensembliste de cet ensemble avec l'ensemble spécifié.

Parameters:
ens - L'ensemble avec lequel l'intersection doit etre effectuée.
Returns:
L'intersection ensembliste de cet ensemble avec l'ensemble spécifié
Specifications: pure
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();

difference

public PureEnsemble difference(PureEnsemble ens)
Renvoie l'ensemble représentant la différence ensembliste de cet ensemble avec l'ensemble spécifié.

Parameters:
ens - L'ensemble à soustraire de cet ensemble.
Returns:
La différence ensembliste de cet ensemble avec l'ensemble spécifié
Specifications: pure
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();

estVide

public boolean estVide()
Teste si cet ensemble ne contient aucun élément.

Returns:
true si cet ensemble ne contient aucun élément ; false sinon.
Specifications: pure
ensures \result <==> (this.cardinal() == 0);

cardinal

public int cardinal()
Renvoie le cardinal de cet ensemble.

Returns:
le nombre d'éléments de cet ensemble.
Specifications: pure
ensures \result >= 0;

tabElements

public java.lang.Object[] tabElements()
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.

Returns:
Un tableau contenant tous les éléments de cet ensemble.
Specifications: pure
ensures \result != null;
ensures \fresh(\result );
ensures \result .length == this.cardinal();
ensures ( \forall int i; i >= 0&&i < \result .length; this.contient(\result [i]));
ensures ( \forall java.lang.Object o; this.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]));

equals

public boolean equals(java.lang.Object obj)
Teste l'égalité entre l'objet spécifié et cet ensemble. Renvoie true si et seulement si l'objet spécifié est aussi un Ensemble, que les deux ensembles ont le même nombre d'éléments et que les deux ensembles contiennent les mêmes elements au sens de equals .

Parameters:
obj - l'objet à comparer avec cette liste.
Returns:
true si l'objet spécifié est composé d'éléments equals à ceux de cette liste ; false sinon
Specifications: pure
     also
ensures !(obj instanceof PureEnsemble) ==> !\result ;
ensures obj instanceof PureEnsemble ==> (\result <==> (((PureEnsemble)obj).estInclusDans(this)&&this.estInclusDans((PureEnsemble)obj)));
ensures \result ==> this.cardinal() == ((PureEnsemble)obj).cardinal();
ensures (this.cardinal() != ((PureEnsemble)obj).cardinal()) ==> !\result ;
ensures \result ==> (this.hashCode() == ((PureEnsemble)obj).hashCode());
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public normal_behavior
requires obj != null&&\typeof(this) == \type(Object);
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;
     also
requires obj != null;
diverges false;
ensures \result == obj.equals(this);

hashCode

public int hashCode()
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 ens1.equals(ens2) implique que ens1.hashCode()==ens2.hashCode() pour toute paire d'ensembles, ens1 et ens2, comme le spécifie le contrat de Object.hashCode.

Returns:
la valeur du code de hashage pour cet ensemble.
Specifications: pure
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public normal_behavior
requires \typeof(this) == \type(Object);
assignable \nothing;