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é. |
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;