/**
 *  Représentation d'une cellule de liste simplement chainée, dont le contenu
 *  est un objet de type Elem.
 *
 * @author     Marc Champesme
 * @created    4 novembre 2003
 */
public class CellElem {
	private Elem _entry;
	private CellElem _next;


	/**
	 *  Initialise une cellule sans successeur avec la valeur transmise en paramètre
	 *
	 * @param  entry  Valeur a placer comme contenu de la cellule
	 */
	/*@ requires entry != null;
	  @ ensures getEntry() == entry;
	  @ ensures !hasNext();
	  @*/
	public CellElem(Elem entry) {
		_entry = entry;
	}


	/**
	 *  Remplace la cellule suivante par une nouvelle cellule.
	 *
	 * @param  nextCell  La nouvelle cellule suivante
	 */
	/*@ requires !hasNext();
	  @ requires nextCell != null;
	  @ ensures hasNext();
	  @ ensures getNext() == nextCell;
	  @*/
	public void setNext(CellElem nextCell) {

		_next = nextCell;
	}


	/**
	 *  Renvoie l'objet de type Elem contenu dans la cellule.
	 *
	 * @return    La valeur contenue dans la cellule
	 */
	/*@ ensures \result != null;
	  @ pure
	  @*/
	public Elem getEntry() {

		return _entry;
	}


	/**
	 *  Renvoie la cellule suivante
	 *
	 * @return    La cellule suivante
	 */
	/*@
	  @ requires hasNext();
	  @ ensures \result != null;
	  @ pure
	  @*/
	public CellElem getNext() {

		return _next;
	}


	/**
	 *  Teste si la cellule possède une cellule suivante
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ pure
	  @*/
	public boolean hasNext() {

		return _next != null;
	}


	/**
	 *  Supprime la cellule suivante.
	 */
	/*@
	  @ requires hasNext();
	  @ ensures !hasNext();
	  @*/
	public void removeNext() {

		_next = null;
	}
}
// -- end class CellElem