/**
 *  Description of the Class
 *
 * @author     Marc Champesme
 * @version    9 décembre 2004
 */
public class ListeElem {
	private CellElem _premiereCellule;
	private int _nbElements;


	/**
	 *  Constructeur pouvant se substituer à l'opération listevide.
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public ListeElem() { }


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result != this;
	  @ ensures \result.longueur() == longueur();
	  @ ensures !estVide() ==> (\result.premier() == premier());
	  @
	  @ pure
	  @*/
	private ListeElem copie() {
		ListeElem result;
		result = new ListeElem();

		if (!estVide()) {
			result._premiereCellule = new CellElem(premier());

			if (_premiereCellule.hasNext()) {
				CellElem celluleCouranteThis;
				CellElem celluleCouranteResult = result._premiereCellule;

				for (celluleCouranteThis = _premiereCellule.getNext();
					celluleCouranteThis.hasNext();
					celluleCouranteThis = celluleCouranteThis.getNext()) {
					CellElem newCell = new CellElem(celluleCouranteThis.getEntry());
					celluleCouranteResult.setNext(newCell);
					celluleCouranteResult = newCell;
				}
				//@ assume celluleCouranteThis != null;
				//@ assume !celluleCouranteThis.hasNext();

				// Ajout de la derniere cellule
				celluleCouranteResult.setNext(new CellElem(celluleCouranteThis.getEntry()));
			}
		}
		result._nbElements = this._nbElements;

		return result;
	}


	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 */
	/*@
	  @ requires elt != null;
	  @ ensures !estVide();
	  @ ensures premier() == elt;
	  @ ensures longueur() == \old(longueur() + 1);
	  @*/
	public void cons(Elem elt) {
		CellElem oldFirstCell = _premiereCellule;

		_premiereCellule = new CellElem(elt);
		if (oldFirstCell != null) {
			_premiereCellule.setNext(oldFirstCell);
		}
		_nbElements++;
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @
	  @ pure
	  @*/
	public Elem premier() {
		return _premiereCellule.getEntry();
	}


	/**
	 *  Description of the Method
	 */
	/*@
	  @ requires !estVide();
	  @ ensures longueur() == \old(longueur() - 1);
	  @*/
	public void fin() {
		if (_premiereCellule.hasNext()) {
			_premiereCellule = _premiereCellule.getNext();
		} else {
			_premiereCellule = null;
		}
		_nbElements--;
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result <==> (longueur() == 0);
	  @
	  @ pure
	  @*/
	public boolean estVide() {
		return _premiereCellule == null;
	}



	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 * @return      Description of the Return Value
	 */
	/*@
	  @ 	requires estVide();
	  @ 	ensures !\result;
	  @ also
	  @ 	requires !estVide();
	  @ 	ensures (premier() == elt) ==> \result;
	  @
	  @ pure
	  @*/
	public boolean estPresent(Elem elt) {
		if (estVide()) {
			return false;
		} else if (premier() == elt) {
			return true;
		} else if (_premiereCellule.hasNext()) {
			boolean trouve = false;
			CellElem cell = _premiereCellule.getNext();

			for (cell = _premiereCellule.getNext();
				cell.hasNext() && !trouve;
				cell = cell.getNext()) {
				trouve = (cell.getEntry() == elt);
			}
			return trouve || (cell.getEntry() == elt);
		} else {
			// la liste possède une seule cellule et ce n'est pas
			// celle cherchée
			//@ assume longueur() == 1;
			return false;
		}
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result >= 0;
	  @
	  @ pure
	  @*/
	public int longueur() {
		return _nbElements;
	}



	/**
	 *  Description of the Method
	 *
	 * @param  autreListe  Description of the Parameter
	 */
	/*@
	  @ requires autreListe != null;
	  @ ensures !\old(estVide()) ==> (premier() == \old(premier()));
	  @ ensures longueur() == \old(this.longueur() + autreListe.longueur());
	  @
	  @ pure
	  @*/
	public void concatener(ListeElem autreListe) {
		if (!autreListe.estVide()) {
			ListeElem copieAutreListe = autreListe.copie();

			if (this.estVide()) {
				_premiereCellule = copieAutreListe._premiereCellule;
				_nbElements = copieAutreListe._nbElements;
			} else {
				CellElem cell = _premiereCellule;

				for (int i = 1; i < longueur(); i++) {
					cell = cell.getNext();
				}
				//@ assume cell != null;
				//@ assume !cell.hasNext();
				cell.setNext(copieAutreListe._premiereCellule);
				_nbElements += autreListe.longueur();
			}
		}
	}


	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 * @return      Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @ requires estPresent(elt);
	  @ ensures \result >= 1;
	  @ ensures elt == premier() ==> \result == 1;
	  @
	  @ pure
	  @*/
	public int rechercher(Elem elt) {
		int rangEltTrouve = 0;

		if (premier() == elt) {
			rangEltTrouve = 1;
		} else {
			//@ assume _premiereCellule.hasNext();
			CellElem cell = _premiereCellule.getNext();
			int rangEltCourant = 2;

			while (cell.hasNext() && rangEltTrouve == 0) {
				if (cell.getEntry() == elt) {
					rangEltTrouve = rangEltCourant;
				}
				cell = cell.getNext();
				rangEltCourant++;
			}
			//@ assume cell != null;
			//@ assume (rangEltTrouve == 0) ==> !cell.hasNext();
			if (rangEltTrouve == 0) {
				rangEltTrouve = rangEltCourant + 1;
			}
		}
		return rangEltTrouve;
	}
	
	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@ also
	  @ ensures \result != null;
	  @
	  @ pure
	  @*/
	public String toString() {
		if (estVide()) {
			return "nil#0";
		} else {
			String res = "[" + premier();
			CellElem cell = _premiereCellule;

			if (cell.hasNext()) {
				for (cell = cell.getNext(); cell.hasNext(); cell = cell.getNext()) {
					res = res + ", " + cell.getEntry();
				}
				//@ assume cell != null;
				//@ assume !cell.hasNext();
				res = res + ", " + cell.getEntry();
			}

			return res + "]#" + longueur();
		}
	}
}