Class Polygone

java.lang.Object
  Polygone

public class Polygone

extends java.lang.Object

La classe Polygone decrit la notion geometrique usuelle de polygone, c'est a dire, celle d'une figure fermee plane delimitee par un nombre arbitraire de segments, chacun de ces segments formant un cote du polygone. En pratique, chaque instance de la classe Polygone est definie par un tableau d'instances de la classe Point. Chaque element de ce tableau definie un sommet du polygone et deux elements successifs (selon l'ordre que definie le tableau) forment les extremites d'un segment de droite formant un cote du polygone. Le premier et le dernier point sont joints par un segment de droite qui ferme le polygone. Le nombre de sommets d'un polygone est fixe une fois pour toute au moment de la creation de l'objet et ne peut etre modifie. Ce nombre doit etre strictement positif. Seules les modifications des coordonnees des sommets sont permises, mais ne doivent etre possibles que par l'intermediaire des methodes de la classe Polygone.

Version:

0.5 21/02/2002, 0.6 10/03/2004

Author:

Marc Champesme

Class Specifications

invariant this.getNbSommets() > 0; invariant ( \forall int i; i >= 0&&i < this.getNbSommets(); this.getSommet(i) != null); invariant Polygone.getNbPetitsPolygones() >= 0; invariant Polygone.getNbGrandsPolygones() >= 0;

Specifications inherited from class Object

represents objectState <- JMLDataGroup.IT;

Model Field Summary

 

Model fields inherited from class java.lang.Object

objectState

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Polygone(int nbSommets)           Initialise un polygone a nbSommets sommets.

Polygone(Point[] sommets, int nbSommets)           Initialise un polygone a nbSommets sommets.

 

Method Summary
static int	getNbGrandsPolygones()           Renvoie le nombre de grands polygones crees depuis le demarrage de l'application.
static int	getNbPetitsPolygones()           Renvoie le nombre de petits polygones crees depuis le demarrage de l'application.
int	getNbSommets()           Renvoie le nombre de sommets du polygone.
Point	getSommet(int numSommet)           Renvoie une instance de la classe Point dont les coordonnees sont celles du sommet de numero numSommet.
Point[]	getSommets()           Renvoie un tableau de Point de meme coordonnées que les sommets de l'instance courante.
void	setSommet(int numSommet, Point unPoint)           Fixe les coordonnees du sommet de numero numSommet du polygone a la valeur des coordonnees du point unPoint.
java.lang.String	toString()           Renvoie le nom du polygone.

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

Polygone

public Polygone(int nbSommets)

Initialise un polygone a nbSommets sommets. Tous les sommets sont initialises avec des coordonees (0, 0). Les coordonnees de chaque sommet peuvent ensuite etre modifiées individuellement a l'aide de la methode setSommet(int, Point).

Parameters:

nbSommets - Nombre total de sommets du Polygone

Specifications:

requires nbSommets > 0;
ensures this.getNbSommets() == nbSommets;
ensures ( \forall int i; i >= 0&&i < this.getNbSommets(); this.getSommet(i).getX() == 0&&this.getSommet(i).getY() == 0);
ensures (nbSommets < 5) ==> (getNbPetitsPolygones() == \old(getNbPetitsPolygones())+1);
ensures (nbSommets >= 5) ==> (getNbGrandsPolygones() == \old(getNbGrandsPolygones())+1);

Polygone

public Polygone(Point[] sommets,
                int nbSommets)

Initialise un polygone a nbSommets sommets. Les sommets sont initialises a partir des points du tableau sommets.

Parameters:

sommets - les points utilises pour initialises les sommets du polygone

nbSommets - Nombre total de sommets du Polygone

Specifications:

requires nbSommets > 0;
requires sommets != null;
requires sommets.length >= nbSommets;
requires ( \forall int i; i >= 0&&i < nbSommets; sommets[i] != null);
ensures this.getNbSommets() == nbSommets;
ensures ( \forall int i; i >= 0&&i < nbSommets; this.getSommet(i).equals(sommets[i]));
ensures (nbSommets < 5) ==> (getNbPetitsPolygones() == \old(getNbPetitsPolygones())+1);
ensures (nbSommets >= 5) ==> (getNbGrandsPolygones() == \old(getNbGrandsPolygones())+1);

getNbPetitsPolygones

public static int getNbPetitsPolygones()

Renvoie le nombre de petits polygones crees depuis le demarrage de l'application. Un petit polygone est un polygone possedant moins de 5 sommets.

Returns:

nombre de petits polygones crees

Specifications: pure

getNbGrandsPolygones

public static int getNbGrandsPolygones()

Renvoie le nombre de grands polygones crees depuis le demarrage de l'application. Un grand polygone est un polygone possedant 5 sommets ou plus

Returns:

nombre de grands polygones crees

Specifications: pure

setSommet

public void setSommet(int numSommet,
                      Point unPoint)

Fixe les coordonnees du sommet de numero numSommet du polygone a la valeur des coordonnees du point unPoint.

Parameters:

numSommet - numero du sommet a modifier

unPoint - point specifiant les nouvelles coordonnees du sommet a modifier.

Specifications:

requires (numSommet >= 0)&&(numSommet < this.getNbSommets());
requires unPoint != null;
ensures this.getSommet(numSommet).equals(unPoint);

getSommet

public Point getSommet(int numSommet)

Renvoie une instance de la classe Point dont les coordonnees sont celles du sommet de numero numSommet.

Parameters:

numSommet - numero du sommet

Returns:

le sommet de numero numSommet du polygone

Specifications: pure

requires (numSommet >= 0)&&(numSommet < this.getNbSommets());
ensures \result != null;

getNbSommets

public int getNbSommets()

Renvoie le nombre de sommets du polygone.

Returns:

le nombre de sommets du polygone

Specifications: pure

getSommets

public Point[] getSommets()

Renvoie un tableau de Point de meme coordonnées que les sommets de l'instance courante.

Returns:

un tableau de Point de meme coordonnées que les sommets de l'instance courante

Specifications: pure

ensures \result != null;
ensures \result .length == this.getNbSommets();
ensures ( \forall int i; i >= 0&&i < this.getNbSommets(); \result [i] != null);
ensures ( \forall int i; i >= 0&&i < this.getNbSommets(); \result [i].equals(this.getSommet(i)));

toString

public java.lang.String toString()

Renvoie le nom du polygone.

Overrides:

toString in class java.lang.Object

Returns:

le nom du polygone

Specifications: pure

     also

ensures \result != null;

Specifications inherited from overridden method in class Object:

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

     also

public normal_behavior
requires \typeof(this) == \type(Object);
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 model_program { ... }

    implies_that

ensures \result != null;