import java.util.Iterator;

/**
 *  <p>
 *
 *  Version restreinte et francisée de l'interface <code>java.util.List</code>.
 *  </p>
 *
 * @author     Marc Champesme
 * @version    11 janvier 2005
 * @since      11 janvier 2005
 * @see        java.util.List
 */

public interface Liste {
	/*@
	  @ invariant taille() >= 0;
	  @ invariant estVide() <==> (taille() == 0);
	  @*/

	/**
	 *  Renvoie un itérateur en lecture seule (opération remove interdite).
	 *
	 * @return    un itérateur sur les éléments de cette liste.
	 */
	/*@
	  @ ensures \result != null;
	  @
	  @ pure
	  @*/
	public abstract Iterator iterator();


	/**
	 *  Renvoie l'élément situé &agrave; l'index spécifié dans cette liste.
	 *
	 * @param  index  index de l'élément &agrave; renvoyer
	 * @return        l'élément &agrave; la position spécifié dans la liste.
	 */
	/*@
	  @ requires index >= 0 && index < taille();
	  @ ensures contient(\result);
	  @ ensures indexDe(\result) <= index;
	  @ pure
	  @*/
	public Object get(int index);


	/**
	 *  Renvoie <code>true</code> si cette liste contient l'élément spécifié. Plus
	 *  précisément, renvoie <code>true</code> si et seulement si cette liste
	 *  contient au moins un élément <code>e</code> tel que:
	 *  <ul>
	 *    <li> <code>e == null</code> si <code>element == null</code></li>
	 *    <li> <code>element.equals(e)</code> si <code>element != null</code></li>
	 *
	 *  </ul>
	 *
	 *
	 * @param  element  élément dont la présence dans cette liste doit etre testée.
	 * @return          <code>true</code> si l'élement spécifié est présent ;
	 *      <code>false</code> sinon.
	 */
	/*@
	  @ ensures (element == null)
	  @		==> (\result <==> (\exists int i; i >= 0 && i < taille();
	  @							get(i) == null));
	  @ ensures (element != null)
	  @		==> (\result <==> (\exists int i; i >= 0 && i < taille();
	  @						get(i).equals(element)));
	  @
	  @ pure
	  @*/
	public boolean contient(Object element);



	/**
	 *  Recherche dans cette liste de la première occurence de l'élément spécifié.
	 *  C'est la méthode <code>equals</code> qui est utilisée pour tester l'égalité
	 *  de l'élément cherché avec les éléments de la liste.Plus précisément,
	 *  renvoie le plus petit index <code>i</code> tel que:
	 *  <ul>
	 *    <li> <code>get(i) == null</code> si <code>element == null</code></li>
	 *
	 *    <li> <code>element.equals(get(i))</code> si <code>element != null</code>
	 *    </li>
	 *    <li> <code>i == -1</code> si aucun index ne satisfait les conditions
	 *    précédentes</li>
	 *  </ul>
	 *
	 *
	 * @param  element  élément recherché
	 * @return          l'index de la première occurence de l'élément dans cette
	 *      liste ; renvoie -1 si l'objet n'est pas trouvé.
	 */
	/*@
	  @ ensures \result == -1 <==> !contient(element);
	  @ ensures contient(element) <==> (\result >= 0 && \result < taille());
	  @ ensures (contient(element) && element == null) ==>  get(\result) == null;
	  @ ensures (contient(element) && element == null) ==>
	  @			(\forall int i; i >= 0 && i < \result; get(i) != null);
	  @ ensures (contient(element) && element != null) ==> element.equals(get(\result));
	  @ ensures (contient(element) && element != null) ==>
	  @ 			(\forall int i; i >= 0 && i < \result; !element.equals(get(i)));
	  @ pure
	  @*/
	public int indexDe(Object element);


	/**
	 *  Insertion dans la liste de l'élement spécifié &agrave; la position
	 *  spécifiée. Le cas échéant, décale vers la droite l'élément actuellement
	 *  &agrave; cette position ainsi que tous les éléments suivant.
	 *
	 * @param  index    index auquel l'élément spécifié va etre inséré
	 * @param  element  élément &agrave; insérer
	 */
	/*@
	  @ requires 0 <= index && index <= this.taille();
	  @ ensures element == this.get(index);
	  @ ensures (\forall int i; 0 <= i && i < index;
	  @		this.get(i) == \old(this.get(i)));
	  @ ensures (\forall int i; index <= i && i < \old(taille());
	  @		this.get(i+1) == \old(this.get(i)));
	  @
	  @*/
	public void ajouter(int index, Object element);


	/**
	 *  Ajoute l'élément spécifié &agrave; la fin de la liste.
	 *
	 * @param  element  element &agrave; ajouter &agrave; cette liste.
	 */
	/*@
	  @ ensures taille() == \old(taille()) + 1;
	  @ ensures (this.get(\old(taille())) == element);
	  @ ensures (\forall int i; 0 <= i && i < \old(taille());
	  @				this.get(i) == \old(this.get(i)));
	  @*/
	public void ajouter(Object element);



	/**
	 *  Remplace l'élément de cette liste placé &agrave; la position spécifiée par
	 *  l'élément spécifié.
	 *
	 * @param  index    index de l'élément &agrave; remplacer.
	 * @param  element  élément &agrave; placer &agrave; la position spécifiée.
	 * @return          l'élément précédement situé &agrave; la position spécifiée.
	 */
	/*@
	  @ requires index >= 0 && index < taille();
	  @ ensures taille() == \old(taille());
	  @ ensures \result == \old(get(index));
	  @ ensures get(index) == element;
	  @ ensures (\forall int i; 0 <= i && i != index && i < taille();
	  @				this.get(i) ==  \old(this.get(i)));
	  @*/
	public Object set(int index, Object element);


	/**
	 *  Enlève de cette liste l'élément situé &agrave; la position spécifié. Décale
	 *  vers la gauche tous les éléments situés après l'élément supprimé.
	 *
	 * @param  index  l'index de l'élément &agrave; enlever
	 * @return        l'élément enlevé de la liste
	 */
	/*@
	  @ requires index >= 0 && index < taille();
	  @ ensures \result == \old(get(index));
	  @ ensures taille() == \old(taille()) - 1;
	  @ ensures (\forall int i; 0 <= i && i < index;
	  @		this.get(i) == \old(this.get(i)));
	  @ ensures (\forall int i; index < i && i < \old(taille());
	  @		this.get(i-1) == \old(this.get(i)));
	  @*/
	public Object retirer(int index);


	/**
	 *  Enlève tous les éléments de cette liste.
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public void vider();


	/**
	 *  Teste si cette liste ne contient aucun élément.
	 *
	 * @return    <code>true</code> si cette liste ne contient aucun élément ;
	 *      <code>false</code> sinon.
	 */
	/*@
	  @ ensures \result <==> (taille() == 0);
	  @ pure
	  @*/
	public boolean estVide();



	/**
	 *  Renvoie le nombre d'éléments dans cette liste.
	 *
	 * @return    le nombre d'éléments dans cette liste.
	 */
	/*@
	  @ ensures \result >= 0;
	  @ pure
	  @*/
	public int taille();



	/**
	 *  Teste l'égalité entre l'objet spécifié et cette liste. Renvoie <code>true</code>
	 *  si et seulement si l'objet spécifié est aussi une <code>ListeTableau,</code>
	 *  , que les deux listes ont le m&ecirc;me nombre d'éléments et que toutes les
	 *  paires d'éléments correspondants dans les deux listes sont <i>equal</i> .
	 *  En d'autres termes, deux listes sont dites <i>equal</i> si elle contiennent
	 *  les m&ecirc;mes elements dans le m&ecirc;me ordre.
	 *
	 * @param  obj  l'objet &agrave; comparer avec cette liste.
	 * @return      <code>true</code> si l'objet spécifié est <i>equal </i>
	 *      &agrave; cette liste.
	 */
	/*@
	  @ also
	  @ ensures (obj instanceof Liste && this.taille() == ((Liste)obj).taille())
	  @		==> (\result
	  @			<==> (\forall int i; 0 <= i && i < this.taille();
	  @				(this.get(i) == null && ((Liste)obj).get(i) == null)
	  @				|| (this.get(i).equals(((Liste)obj).get(i)))));
	  @ ensures (this == obj) ==> \result;
	  @ ensures !(obj instanceof Liste && this.taille() == ((Liste)obj).taille())
	  @			==> !\result;
	  @ ensures (obj == null) ==> !\result;
	  @ pure
	  @*/
	public boolean equals(Object obj);


	/**
	 *  Renvoie la valeur du code de hashage de cette liste. Le calcul de ce code
	 *  de hashage s'inspire de celui décrit dans la documentation de l'interface
	 *  {@link java.util.List#hashCode() List} de la manière suivante: <pre>
	 *	hashCode = 1;
	 *	Iterator i = list.iterator();
	 *	while (i.hasNext()) {
	 *		Object obj = i.next();
	 *		hashCode = 31*hashCode + (obj==null ? 0 : obj.hashCode());
	 *	}
	 *</pre> <p>
	 *
	 *  Ce calcul assure que <code>list1.equals(list2)</code> implique que <code>list1.hashCode()==list2.hashCode()</code>
	 *  pour toutes listes, <code>list1</code> et <code>list2</code>, comme le
	 *  spécifie le contrat de <code>Object.hashCode</code>.</p>
	 *
	 * @return    la valeur du code de hashage pour cette liste.
	 */
	//@ pure
	public int hashCode();

}