Class EnsembleEntierTab

java.lang.Object
  EnsembleEntierTab

public class EnsembleEntierTab

extends java.lang.Object

EnsembleEntierTab represente un ensemble d'entiers sous la forme d'un tableau.

Class Specifications

public invariant this.estVide() <==> this.getCardinal() == 0; public invariant !this.estVide() ==> this.contient(this.getMin()); public invariant !this.estVide() ==> this.getMin() == ( \min int x; this.contient(x); x); public invariant this.getCapacite() > 0; public invariant 0 <= this.getCardinal()&&this.getCardinal() <= this.getCapacite();

Specifications inherited from class Object

public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

EnsembleEntierTab(int taille_)           Construction d'un ensemble de capacite taille_.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	ajouter(int x)           Ajouter l'element x dans l'ensemble.
boolean	contient(int x)           Est-ce que x appartient a l'ensemble ?
boolean	estVide()           Est-ce que l'ensemble est vide ?
int	getCapacite()           getCapacite renvoie la capacite de l'ensemble.
int	getCardinal()           getCardinal renvoie le cardinal de l'ensemble.
int	getMin()           Le plus petit element de l'ensemble.
void	oter(int x)           Enlever l'element x de l'ensemble.
java.lang.String	toString()           Une representation de l'ensemble sous forme de chaine de caracteres, comme par exemple "{ 1, 5, 2 }".

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Constructor Detail

EnsembleEntierTab

public EnsembleEntierTab(int taille_)

Construction d'un ensemble de capacite taille_.

Parameters:

taille_ - contenance de l'ensemble

Specifications:

requires taille_ > 0;
ensures this.getCardinal() == 0;
ensures this.getCapacite() == taille_;

getCapacite

public int getCapacite()

getCapacite renvoie la capacite de l'ensemble.

Returns:

un entier qui est la capacite maximale de l'ensemble

Specifications: pure

getCardinal

public int getCardinal()

getCardinal renvoie le cardinal de l'ensemble.

Returns:

un entier qui est le nombre d'elements de l'ensemble

Specifications: pure

estVide

public boolean estVide()

Est-ce que l'ensemble est vide ?

Returns:

un booleen qui vaut true si l'ensemble est vide

Specifications: pure

contient

public boolean contient(int x)

Est-ce que x appartient a l'ensemble ?

Parameters:

x - un int qui est l'element cherche

Returns:

un booleen qui est true si x appartient a l'ensemble

Specifications: pure

ajouter

public void ajouter(int x)

Ajouter l'element x dans l'ensemble.

Parameters:

x - l'element a ajouter

Specifications:

requires !this.contient(x) ==> this.getCardinal() < this.getCapacite();
ensures this.contient(x);
ensures !\old(this.contient(x)) ==> this.getCardinal() == \old(this.getCardinal())+1;
ensures \old(this.contient(x)) ==> this.getCardinal() == \old(this.getCardinal());

oter

public void oter(int x)

Enlever l'element x de l'ensemble.

Parameters:

x - l'element a supprimer

Specifications:

ensures !this.contient(x);
ensures !\old(this.contient(x)) ==> this.getCardinal() == \old(this.getCardinal());
ensures \old(this.contient(x)) ==> this.getCardinal() == \old(this.getCardinal())-1;

getMin

public int getMin()

Le plus petit element de l'ensemble.

Returns:

un entier qui est le plus petit element de l'ensemble

Specifications: pure

requires !this.estVide();
ensures this.contient(\result );
ensures \result == ( \min int x; this.contient(x); x);

toString

public java.lang.String toString()

Une representation de l'ensemble sous forme de chaine de caracteres, comme par exemple "{ 1, 5, 2 }".

Overrides:

toString in class java.lang.Object

Returns:

une representation sous forme de String de l'ensemble

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;