/**
 *  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.
 *
 * @author     Marc Champesme
 * @version    0.5 21/02/2002
 * @version    0.6 10/03/2004
 */

public class Polygone {
	/*@
	  @ invariant getNbSommets() > 0;
	  @ invariant (\forall int i; i >= 0 && i < getNbSommets(); getSommet(i) != null);
	  @ invariant Polygone.getNbPetitsPolygones() >= 0;
	  @ invariant Polygone.getNbGrandsPolygones() >= 0;
	  @*/
	private static int compteurDInstances;
	private static int nbPetitsPolygones;
	private static int nbGrandsPolygones;
	private Point[] sommets;
	private int nbSommets;
	private String monNom;


	/**
	 *  Renvoie le nombre de petits polygones crees depuis le demarrage de
	 *  l'application. Un petit polygone est un polygone possedant moins de 5
	 *  sommets.
	 *
	 * @return    nombre de petits polygones crees
	 */
	/*@
	  @ pure
	  @*/
	public static int getNbPetitsPolygones() {
		return Polygone.nbPetitsPolygones;
	}


	/**
	 *  Renvoie le nombre de grands polygones crees depuis le demarrage de
	 *  l'application. Un grand polygone est un polygone possedant 5 sommets ou
	 *  plus
	 *
	 * @return    nombre de grands polygones crees
	 */
	/*@
	  @ pure
	  @*/
	public static int getNbGrandsPolygones() {
		return Polygone.nbGrandsPolygones;
	}


	/**
	 *  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).
	 *
	 * @param  nbSommets  Nombre total de sommets du Polygone
	 */
	/*@
	  @ requires nbSommets > 0;
	  @ ensures getNbSommets() == nbSommets;
	  @ ensures (\forall int i; i >= 0 && i < getNbSommets();
	  @			getSommet(i).getX() == 0 && getSommet(i).getY() == 0);
	  @ ensures (nbSommets < 5) ==>
	  		(getNbPetitsPolygones() == \old(getNbPetitsPolygones()) + 1);
	  @ ensures (nbSommets >= 5) ==>
	 		(getNbGrandsPolygones() == \old(getNbGrandsPolygones()) + 1);
	  @*/
	public Polygone(int nbSommets) {
		this.sommets = new Point[nbSommets];
		// Il faut maintenant creer les objets Point, car la creation
		// du tableau se contente d'initialiser chaque element a null
		for (int i = 0; i < nbSommets; i++) {
			this.sommets[i] = new Point();
		}
		compteurDInstances++;
		monNom = "polygone#" + compteurDInstances;
		if (nbSommets < 5) {
			nbPetitsPolygones++;
		} else {
			nbGrandsPolygones++;
		}
	}


	/**
	 *  Initialise un polygone a nbSommets sommets. Les sommets sont initialises a
	 *  partir des points du tableau sommets.
	 *
	 * @param  sommets    les points utilises pour initialises les sommets du
	 *      polygone
	 * @param  nbSommets  Nombre total de sommets du Polygone
	 */
	/*@
	  @ requires nbSommets > 0;
	  @ requires sommets != null;
	  @ requires sommets.length >= nbSommets;
	  @ requires (\forall int i; i >= 0 && i < nbSommets;
	  					sommets[i] != null);
	  @
	  @ ensures getNbSommets() == nbSommets;
	  @ ensures (\forall int i; i >= 0 && i < nbSommets;
	  					getSommet(i).equals(sommets[i]));
	  @ ensures (nbSommets < 5) ==>
	 		(getNbPetitsPolygones() == \old(getNbPetitsPolygones()) + 1);
	  @ ensures (nbSommets >= 5) ==>
	 		(getNbGrandsPolygones() == \old(getNbGrandsPolygones()) + 1);
	  @
	  @*/
	public Polygone(Point[] sommets, int nbSommets) {
		this.sommets = new Point[nbSommets];
		for (int i = 0; i < nbSommets; i++) {
			this.sommets[i] = new Point(sommets[i]);
		}
		this.nbSommets = nbSommets;
		compteurDInstances++;
		monNom = "polygone#" + compteurDInstances;
		if (nbSommets < 5) {
			nbPetitsPolygones++;
		} else {
			nbGrandsPolygones++;
		}
	}


	/**
	 *  Fixe les coordonnees du sommet de numero numSommet du polygone a la valeur
	 *  des coordonnees du point unPoint.
	 *
	 * @param  numSommet  numero du sommet a modifier
	 * @param  unPoint    point specifiant les nouvelles coordonnees du sommet a
	 *      modifier.
	 */
	/*@
	  @ requires (numSommet >= 0) && (numSommet < getNbSommets());
	  @ requires unPoint != null;
	  @ ensures getSommet(numSommet).equals(unPoint);
	  @*/
	public void setSommet(int numSommet, Point unPoint) {
		sommets[numSommet] = new Point(unPoint);
	}


	/**
	 *  Renvoie une instance de la classe Point dont les coordonnees sont celles du
	 *  sommet de numero numSommet.
	 *
	 * @param  numSommet  numero du sommet
	 * @return            le sommet de numero numSommet du polygone
	 */
	/*@
	  @ requires (numSommet >= 0) && (numSommet < getNbSommets());
	  @ ensures \result != null;
	  @ pure
	  @*/
	public Point getSommet(int numSommet) {
		return sommets[numSommet];
	}


	/**
	 *  Renvoie le nombre de sommets du polygone.
	 *
	 * @return    le nombre de sommets du polygone
	 */
	//@ pure
	public int getNbSommets() {
		return nbSommets;
	}


	/**
	 *  Renvoie un tableau de Point de meme coordonnées que les sommets de
	 *  l'instance courante.
	 *
	 * @return    un tableau de Point de meme coordonnées que les sommets de
	 *      l'instance courante
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.length == getNbSommets();
	  @ ensures (\forall int i; i >= 0 && i < getNbSommets();
	  				\result[i] != null);
	  @ ensures (\forall int i; i >= 0 && i < getNbSommets();
	  				\result[i].equals(getSommet(i)));
	  @
	  @ pure
	  @*/
	  public Point[] getSommets() {
		  Point[] resultat;
		  
		  resultat = new Point[getNbSommets()];
		  for (int i = 0; i >= 0 && i < getNbSommets(); i++) {
			  resultat[i] = getSommet(i);
		  }
	
		return resultat;
	}


	/**
	 *  Renvoie le nom du polygone.
	 *
	 * @return    le nom du polygone
	 */
	/*@ also
	  @ ensures \result != null;
	  @ pure
	  @*/
	public String toString() {
		return monNom;
	}

}