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


	/**
	 *  Constructeur pouvant se substituer à l'opération listevide.
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public PureListeElem() { }


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result != this;
	  @
	  @ pure
	  @*/
	private PureListeElem copie() {
		PureListeElem result = new PureListeElem();

		// A compléter...
		
		return result;
	}


	/**
	 *  Adds a feature to the PureListeElem object
	 *
	 * @param  elt  The feature to be added
	 * @return      Description of the Return Value
	 */
	/*@
	  @ requires 
	  @ ensures \result != null;
	  @ ensures !\result.estVide();
	  @ ensures \result.premier().equals(elt);
	  @ ensures \result.longueur() == (longueur() + 1);
	  @
	  @ pure
	  @*/
	public PureListeElem cons(Elem elt) {
		PureListeElem result = new PureListeElem();

		result._premiereCellule = new CellElem(elt);
		result._nbElements = _nbElements + 1;
		if (!estVide()) {
			PureListeElem copieThis = copie();
			result._premiereCellule.setNext(copieThis._premiereCellule);
		}

		return result;
	}



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


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @ ensures \result != null;
	  @ ensures \result.longueur() == longueur() - 1;
	  @
	  @ pure
	  @*/
	public PureListeElem fin() {
		PureListeElem result = new PureListeElem();

		if (_premiereCellule.hasNext()) {
			PureListeElem copieThis = copie();
			result._premiereCellule = copieThis._premiereCellule.getNext();
			result._nbElements = _nbElements - 1;
		}

		return result;
	}



	/**
	 *  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;
	  @ 	ensures (premier() != elt) ==> (\result <==> fin().estPresent(elt));
	  @
	  @ pure
	  @*/
	public boolean estPresent(Elem elt) {
		
		// A compléter
		
		return true;
	}



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



	/**
	 *  Description of the Method
	 *
	 * @param  liste  Description of the Parameter
	 * @return        Description of the Return Value
	 */
	/*@
	  @ requires liste != null;
	  @ ensures \result != null;
	  @ ensures !estVide() ==> \result.premier().equals(premier());
	  @ ensures \result.longueur() == (this.longueur() + liste.longueur());
	  @
	  @ pure
	  @*/
	public PureListeElem concatener(PureListeElem liste) {
		
		// A compléter
		
		return null;
	}


	/**
	 *  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.equals(premier()) ==> \result == 1;
	  @ ensures elt.equals(premier()) ==> \result == fin().rechercher(elt) + 1;
	  @
	  @ pure
	  @*/
	public int rechercher(Elem elt) {
		int rangEltTrouve = 0;
		
		// A compléter

		return rangEltTrouve;
	}

}