Class Scene

java.lang.Object
  Scene

public class Scene

extends java.lang.Object

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

Version:

Créé mardi 30 mars 2004, Modifié le 6 avril 2004

Author:

Marc Champesme

Class Specifications

invariant this.getNbPolygones() >= 0; invariant ( \forall int i; i >= 0&&i < this.getNbPolygones(); this.getPolygone(i) != null);

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

Scene()           Initialise une instance de la classe Scene de sorte qu'elle représente une scéne vide ne contenant aucun polygone.

 

Method Summary
void	ajouter(Polygone unPolygone)           Ajoute le polygone passé en argument à la scène
void	deplacerEnArriere(Polygone unPolygone)           Déplace le polygone passé en paramètre d'une place vers l'arrière dans la scène.
void	deplacerEnAvant(Polygone unPolygone)           Déplace le polygone passé en paramètre d'une place vers l'avant dans la scène.
boolean	estPresent(Polygone unPolygone)           Détermine si le polygone passé en paramètre est présent dans la scène.
int	getNbPolygones()           Renvoie le nombre de polygones présents dans la scène.
Polygone	getPolygone(int index)           Renvoie le polygone présent dans la scène à l'index fourni en paramêtre.
int	indexDe(Polygone unPolygone)           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.
void	mettreDerriere(Polygone unPolygone)           Met le polygone passé en paramètre à l'arrière plan de la scène.
void	mettreDevant(Polygone unPolygone)           Met le polygone passé en paramètre au premier plan de la scène.
void	retirer(Polygone unPolygone)           Retire de la scène le polygone passé en argument

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

Scene

public Scene()

Initialise une instance de la classe Scene de sorte qu'elle représente une scéne vide ne contenant aucun polygone.

Specifications:

ensures this.getNbPolygones() == 0;

getNbPolygones

public int getNbPolygones()

Renvoie le nombre de polygones présents dans la scène.

Returns:

Le nombre de polygones présents dans la scène

Specifications: pure

ajouter

public void ajouter(Polygone unPolygone)

Ajoute le polygone passé en argument à la scène

Parameters:

unPolygone - Le polygone à ajouter à la scène.

Specifications:

requires unPolygone != null;
requires !this.estPresent(unPolygone);
ensures this.getNbPolygones() == \old(this.getNbPolygones())+1;
ensures this.getPolygone(this.getNbPolygones()-1) == unPolygone;
ensures ( \forall int i; i >= 0&&i < \old(this.getNbPolygones()); this.getPolygone(i) == \old(this.getPolygone(i)));

retirer

public void retirer(Polygone unPolygone)

Retire de la scène le polygone passé en argument

Parameters:

unPolygone - Le polygone à retirer de la scène

Specifications:

requires unPolygone != null;
requires this.estPresent(unPolygone);
ensures !this.estPresent(unPolygone);
ensures this.getNbPolygones() == \old(this.getNbPolygones())-1;
ensures ( \forall int i; i >= 0&&i < \old(this.indexDe(unPolygone)); this.getPolygone(i) == \old(this.getPolygone(i)));
ensures ( \forall int i; i >= \old(this.indexDe(unPolygone))&&i < this.getNbPolygones(); this.getPolygone(i) == \old(this.getPolygone(i+1)));

mettreDevant

public void mettreDevant(Polygone unPolygone)

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.

Parameters:

unPolygone - le polygone à mettre au premier plan, il est supposé être déjà présent dans la scène.

Specifications:

requires unPolygone != null;
requires this.estPresent(unPolygone);
ensures this.getPolygone(this.getNbPolygones()-1) == unPolygone;
ensures this.getNbPolygones() == \old(this.getNbPolygones());
ensures ( \forall int i; i >= 0&&i < \old(this.indexDe(unPolygone)); this.getPolygone(i) == \old(this.getPolygone(i)));
ensures ( \forall int i; i >= \old(this.indexDe(unPolygone))&&i < (this.getNbPolygones()-1); this.getPolygone(i) == \old(this.getPolygone(i+1)));

mettreDerriere

public void mettreDerriere(Polygone unPolygone)

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.

Parameters:

unPolygone - le polygone à mettre à l'arrière plan, il est supposé être déjà présent dans la scène.

Specifications:

requires unPolygone != null;
requires this.estPresent(unPolygone);
ensures this.getPolygone(0) == unPolygone;
ensures this.getNbPolygones() == \old(this.getNbPolygones());
ensures ( \forall int i; i > 0&&i <= \old(this.indexDe(unPolygone)); this.getPolygone(i) == \old(this.getPolygone(i-1)));
ensures ( \forall int i; i > \old(this.indexDe(unPolygone))&&i < this.getNbPolygones(); this.getPolygone(i) == \old(this.getPolygone(i)));

deplacerEnAvant

public void deplacerEnAvant(Polygone unPolygone)

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.

Parameters:

unPolygone - le polygone à avancer d'une place, il est supposé être déjà présent dans la scène.

Specifications:

requires unPolygone != null;
requires this.estPresent(unPolygone);
requires this.indexDe(unPolygone) < this.getNbPolygones()-1;
ensures this.indexDe(unPolygone) == \old(this.indexDe(unPolygone))+1;
ensures this.getPolygone(this.indexDe(unPolygone)-1) == \old(this.getPolygone(this.indexDe(unPolygone)+1));
ensures this.getNbPolygones() == \old(this.getNbPolygones());
ensures ( \forall int i; (i >= 0&&i < this.indexDe(unPolygone)-1)||(i > this.indexDe(unPolygone)&&i < this.getNbPolygones()); this.getPolygone(i) == \old(this.getPolygone(i)));

deplacerEnArriere

public void deplacerEnArriere(Polygone unPolygone)

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.

Parameters:

unPolygone - Le polygone à déplacer d'une place vers l'arrière, il est supposé être déjà présent dans la scène

Specifications:

requires unPolygone != null;
requires this.estPresent(unPolygone);
requires this.indexDe(unPolygone) > 0;
ensures this.indexDe(unPolygone) == \old(this.indexDe(unPolygone))-1;
ensures this.getPolygone(this.indexDe(unPolygone)+1) == \old(this.getPolygone(this.indexDe(unPolygone)-1));
ensures this.getNbPolygones() == \old(this.getNbPolygones());
ensures ( \forall int i; (i >= 0&&i < this.indexDe(unPolygone))||(i > this.indexDe(unPolygone)+1&&i < this.getNbPolygones()); this.getPolygone(i) == \old(this.getPolygone(i)));

indexDe

public int indexDe(Polygone unPolygone)

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.

Parameters:

unPolygone - Le polygone dont on souhaite connaître l'index

Returns:

index du polygone dans la scene

Specifications: pure

requires unPolygone != null;
requires this.estPresent(unPolygone);
ensures \result >= 0&&\result < this.getNbPolygones();
ensures this.getPolygone(\result ) == unPolygone;

estPresent

public boolean estPresent(Polygone unPolygone)

Détermine si le polygone passé en paramètre est présent dans la scène.

Parameters:

unPolygone - Le polygone cherché

Returns:

true si le polygone est présent dans la scène, false sinon.

Specifications: pure

requires unPolygone != null;
ensures \result <==> ( \exists int i; i >= 0&&i < this.getNbPolygones(); this.getPolygone(i) == unPolygone);

getPolygone

public Polygone getPolygone(int index)

Renvoie le polygone présent dans la scène à l'index fourni en paramêtre.

Parameters:

index - Index du polygone cherché

Returns:

Le polygone présent dans la scène à l'index fourni

Specifications: pure

requires index >= 0&&index < this.getNbPolygones();
ensures this.estPresent(\result );
ensures this.indexDe(\result ) == index;