/**
* Une scène est constituée par une liste ordonnée de polygones dont
* l'affichage s'effectue en parcourant cette liste dans l'ordre. Par
* conséquent, le premier polygone de la liste est le plus éloigné de la scène.
* Les principales fonctionnalités de cette classe sont :
*
* - Création d'une scene et ajout d'un polygone dans la scène
* - Déplacement d'un polygone en avant et en arrière d'une place
*
* - Déplacement d'un polygone à l'arrière plan
* - Déplacement d'un polygone au premier plan
* - Suppression d'un polygone
*
*
*
* @author Marc Champesme
* @version Créé mardi 30 mars 2004
* @version Modifié le 6 avril 2004
*/
public class Scene {
/*@
@ invariant getNbPolygones() >= 0;
@ invariant (\forall int i; i >= 0 && i < getNbPolygones();
getPolygone(i) != null);
@*/
private Polygone[] polygones;
private int nbPolygones;
/**
* Initialise une instance de la classe Scene de sorte qu'elle
* représente une scéne vide ne contenant aucun polygone.
*/
/*@
@ ensures getNbPolygones() == 0;
@*/
public Scene() {
polygones = new Polygone[5];
}
/**
* Renvoie le nombre de polygones présents dans la scène.
*
* @return Le nombre de polygones présents dans la scène
*/
//@ pure
public int getNbPolygones() {
return nbPolygones;
}
/**
* Ajoute le polygone passé en argument à la scène
*
* @param unPolygone Le polygone à ajouter à la scène.
*/
/*@
@ requires unPolygone != null;
@ requires !estPresent(unPolygone);
@ ensures getNbPolygones() == \old(getNbPolygones()) + 1;
@ ensures getPolygone(getNbPolygones() - 1) == unPolygone;
@ ensures (\forall int i; i >= 0 && i < \old(getNbPolygones());
getPolygone(i) == \old(getPolygone(i)));
@*/
public void ajouter(Polygone unPolygone) {
if (nbPolygones == polygones.length) {
Polygone[] newTabPoly;
newTabPoly = new Polygone[polygones.length + 10];
for (int i = 0; i < nbPolygones; i++) {
newTabPoly[i] = polygones[i];
}
polygones = newTabPoly;
}
polygones[nbPolygones] = unPolygone;
nbPolygones++;
}
/**
* Retire de la scène le polygone passé en argument
*
* @param unPolygone Le polygone à retirer de la scène
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ ensures !estPresent(unPolygone);
@ ensures getNbPolygones() == \old(getNbPolygones()) - 1;
@ ensures (\forall int i; i >= 0 && i < \old(indexDe(unPolygone));
getPolygone(i) == \old(getPolygone(i)));
@ ensures (\forall int i; i >= \old(indexDe(unPolygone)) && i < getNbPolygones();
getPolygone(i) == \old(getPolygone(i+1)));
@*/
public void retirer(Polygone unPolygone) {
int index = indexDe(unPolygone);
nbPolygones--;
for (int i = index; i < nbPolygones; i++) {
polygones[i] = polygones[i + 1];
}
}
/**
* Met le polygone passé en paramètre au premier plan de la scène. Le polygone
* à déplacer doit déjà faire partie de la scène. Après
* déplacement de ce polygone il devient le polygone d'index le plus élevé
* dans la scène. Lorsque ce déplacement nécessite que le polygone change de
* position, les index des polygones qui, avant le déplacement, étaient devant
* lui voient leur index diminuer d'une unité ; ils reculent donc d'une place
* dans la scène. Les polygones qui étaient derrière le polygone déplacé
* restent à la même place dans la scène.
*
* @param unPolygone le polygone à mettre au premier plan, il est
* supposé être déjà présent dans la scène.
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ ensures getPolygone(getNbPolygones() - 1) == unPolygone;
@ ensures getNbPolygones() == \old(getNbPolygones());
@ ensures (\forall int i; i >= 0 && i < \old(indexDe(unPolygone));
getPolygone(i) == \old(getPolygone(i)));
@ ensures (\forall int i; i >= \old(indexDe(unPolygone)) && i < (getNbPolygones() - 1);
getPolygone(i) == \old(getPolygone(i+1)));
@*/
public void mettreDevant(Polygone unPolygone) {
int index = indexDe(unPolygone);
Polygone temp;
temp = polygones[index];
for (int i = index; i < (nbPolygones - 1); i++) {
polygones[i] = polygones[i + 1];
}
polygones[nbPolygones - 1] = temp;
}
/**
* Met le polygone passé en paramètre à l'arrière plan de la scène. Le
* polygone à déplacer doit déjà faire partie de la scène. Après
* déplacement de ce polygone il devient le polygone d'index 0. Lorsque ce
* déplacement nécessite que le polygone change de position, les index des
* polygones qui, avant le déplacement, étaient derrière lui voient leur index
* augmenter d'une unité ; ils avancent donc d'une place dans la scène. Les
* polygones qui étaient devant le polygone déplacé restent à la même
* place dans la scène.
*
* @param unPolygone le polygone à mettre à l'arrière plan, il
* est supposé être déjà présent dans la scène.
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ ensures getPolygone(0) == unPolygone;
@ ensures getNbPolygones() == \old(getNbPolygones());
@ ensures (\forall int i; i > 0 && i <= \old(indexDe(unPolygone));
getPolygone(i) == \old(getPolygone(i-1)));
@ ensures (\forall int i; i > \old(indexDe(unPolygone)) && i < getNbPolygones();
getPolygone(i) == \old(getPolygone(i)));
@*/
public void mettreDerriere(Polygone unPolygone) {
int index = indexDe(unPolygone);
Polygone temp;
temp = polygones[index];
for (int i = index; i > 0; i--) {
polygones[i] = polygones[i - 1];
}
polygones[0] = temp;
}
/**
* Déplace le polygone passé en paramètre d'une place vers l'avant dans la
* scène. Le polygone à déplacer doit déjà faire partie de la
* scène et ne pas être au premier plan. Ce déplacement s'effectue en
* échangeant la place de ce polygone avec celle du polygone qui était
* immédiatement devant lui. Après déplacement de ce polygone son index
* augmente d'une unité. A l'exception du polygone qui était immédiatement
* devant le polygone déplacé, tous les autres polygones de la scène restent
* à la même place dans la scène.
*
* @param unPolygone le polygone à avancer d'une place, il est supposé
* être déjà présent dans la scène.
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ requires indexDe(unPolygone) < getNbPolygones() - 1;
@ ensures indexDe(unPolygone) == \old(indexDe(unPolygone)) + 1;
@ ensures getPolygone(indexDe(unPolygone) - 1) == \old(getPolygone(indexDe(unPolygone) + 1));
@ ensures getNbPolygones() == \old(getNbPolygones());
@ ensures (\forall int i; (i >= 0 && i < indexDe(unPolygone) - 1)
|| (i > indexDe(unPolygone)
&& i < getNbPolygones());
getPolygone(i) == \old(getPolygone(i)));
@*/
public void deplacerEnAvant(Polygone unPolygone) {
int index = indexDe(unPolygone);
Polygone temp;
temp = polygones[index];
polygones[index] = polygones[index + 1];
polygones[index + 1] = temp;
}
/**
* Déplace le polygone passé en paramètre d'une place vers l'arrière dans la
* scène. Le polygone à déplacer doit déjà faire partie de la
* scène et ne pas être au dernier plan. Ce déplacement s'effectue en
* échangeant la place de ce polygone avec celle du polygone qui était
* immédiatement derrière lui. Après déplacement de ce polygone son index
* diminue d'une unité. A l'exception du polygone qui était immédiatement
* derrière le polygone déplacé, tous les autres polygones de la scène restent
* à la même place dans la scène.
*
* @param unPolygone Le polygone à déplacer d'une place vers
* l'arrière, il est supposé être déjà présent dans la scène
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ requires indexDe(unPolygone) > 0;
@ ensures indexDe(unPolygone) == \old(indexDe(unPolygone)) - 1;
@ ensures getPolygone(indexDe(unPolygone) + 1) == \old(getPolygone(indexDe(unPolygone) - 1));
@ ensures getNbPolygones() == \old(getNbPolygones());
@ ensures (\forall int i; (i >= 0 && i < indexDe(unPolygone))
|| (i > indexDe(unPolygone) + 1
&& i < getNbPolygones());
getPolygone(i) == \old(getPolygone(i)));
@*/
public void deplacerEnArriere(Polygone unPolygone) {
int index = indexDe(unPolygone);
Polygone temp;
temp = polygones[index];
polygones[index] = polygones[index - 1];
polygones[index - 1] = temp;
}
/**
* Renvoie l'index dans la scène (i.e. index permettant d'accéder à ce
* polygone à l'aide de la méthode getPolygone) du
* polygone passé en paramètre. Le polygone cherché doit être présent dans la
* scène. Cet index correspond en même temps à la place du polygone
* dans la scène: plus cet index est élevé, plus il est en avant dans la
* scène.
*
* @param unPolygone Le polygone dont on souhaite connaître l'index
* @return index du polygone dans la scene
*/
/*@
@ requires unPolygone != null;
@ requires estPresent(unPolygone);
@ ensures \result >= 0 && \result < getNbPolygones();
@ ensures getPolygone(\result) == unPolygone;
@ pure
@*/
public int indexDe(Polygone unPolygone) {
int index = -1;
for (int i = 0; i < nbPolygones && index == -1; i++) {
if (polygones[i] == unPolygone) {
index = i;
}
}
return index;
}
/**
* Détermine si le polygone passé en paramètre est présent dans la scène.
*
* @param unPolygone Le polygone cherché
* @return true si le polygone est présent dans la
* scène, false sinon.
*/
/*@
@ requires unPolygone != null;
@ ensures \result <==> (\exists int i; i >= 0 && i < getNbPolygones();
getPolygone(i) == unPolygone);
@ pure
@*/
public boolean estPresent(Polygone unPolygone) {
boolean trouve = false;
for (int i = 0; i < nbPolygones && !trouve; i++) {
trouve = (polygones[i] == unPolygone);
}
return trouve;
}
/**
* Renvoie le polygone présent dans la scène à l'index fourni en
* paramêtre.
*
* @param index Index du polygone cherché
* @return Le polygone présent dans la scène à l'index fourni
*/
/*@
@ requires index >= 0 && index < getNbPolygones();
@ ensures estPresent(\result);
@ ensures indexDe(\result) == index;
@ pure
@*/
public Polygone getPolygone(int index) {
return polygones[index];
}
}