/**
 *  Description of the Class
 *
 * @author     Marc Champesme
 * @version    24 novembre 2004
 */
public class PurePileElem {
	//@ private constraint PILE_VIDE == \old(PILE_VIDE);
	private static PurePileElem PILE_VIDE = new PurePileElem();
	private Elem[] _contenu;
	private int _nbElements;


	/**
	 *  Générateur for the PileElem object
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.hauteur() == 0;
	  @
	  @ pure
	  @*/
	public static PurePileElem pilevide() {
		return PILE_VIDE;
	}


	/**
	 *  Constructor for the PurePileElem object
	 */
	/*@
	  @ ensures equals(PurePileElem.pilevide());
	  @ 
	  @*/
	private PurePileElem() {
		this(0);
	}


	/**
	 *  Constructor for the PurePileElem object
	 *
	 * @param  capacite  Description of the Parameter
	 */
	/*@
	  @ requires capacite >= 0;
	  @ ensures equals(PurePileElem.pilevide());
	  @*/
	private PurePileElem(int capacite) {
		_contenu = new Elem[capacite];
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !equals(PurePileElem.pilevide());
	  @ ensures \result != null;
	  @ ensures \result.hauteur() == hauteur() - 1;
	  @  
	  @ pure
	  @*/
	public PurePileElem depiler() {
		// Nécessite : not estVide()

		if (_nbElements == 1) {
			return PILE_VIDE;
		}

		PurePileElem pileAux = new PurePileElem(_nbElements - 1);

		for (int i = 0; i < _nbElements - 1; i++) {
			pileAux._contenu[i] = _contenu[i];
		}
		pileAux._nbElements = _nbElements - 1;

		return pileAux;
		// Propriété terminale: \result.hauteur() == hauteur() - 1;
	}


	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 * @return      Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.depiler().equals(this);
	  @ ensures \result.hauteur() == hauteur() + 1;
	  @ ensures !\result.equals(PurePileElem.pilevide());
	  @ ensures \result.sommet() == elt;
	  @
	  @ pure
	  @*/
	public PurePileElem empiler(Elem elt) {
		PurePileElem pileAux = new PurePileElem(_nbElements + 1);

		for (int i = 0; i < _nbElements; i++) {
			pileAux._contenu[i] = _contenu[i];
		}
		pileAux._contenu[_nbElements] = elt;
		pileAux._nbElements = _nbElements + 1;

		return pileAux;
		// Propriété terminale: not estVide(this)
		// 				&& sommet(this) == elt
		// 				&& depiler(this) == \old(this)
		// 				&& hauteur(this) == \old(hauteur(this)) + 1;
	}


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result >= 0;
	  @ ensures \result == 0 <==> equals(PurePileElem.pilevide());
	  @
	  @ pure
	  @*/
	public int hauteur() {
		return _nbElements;
	}


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !equals(PurePileElem.pilevide());
	  @
	  @ pure
	  @*/
	public Elem sommet() {
		// Nécessite : not estVide(this)
		return _contenu[_nbElements - 1];
	}


	/**
	 *  Description of the Method
	 *
	 * @param  autrePile  Description of the Parameter
	 * @return            Description of the Return Value
	 */
	/*@
	  @   requires autrePile == null;
	  @   ensures !\result;
	  @ also
	  @   requires autrePile != null;
	  @   ensures hauteur() != autrePile.hauteur() ==> !\result;
	  @ also
	  @   requires autrePile != null;
	  @   requires hauteur() == 0 || autrePile.hauteur() == 0;
	  @   ensures \result <==> hauteur() == autrePile.hauteur();
	  @ also
	  @   requires autrePile != null;
	  @   requires hauteur() > 0;
	  @   requires autrePile.hauteur() > 0;
	  @   ensures \result <==> (sommet() == autrePile.sommet()
	  @   			   && depiler().equals(autrePile.depiler()));
	  @
	  @ pure
	  @*/
	public boolean equals(PurePileElem autrePile) {
		boolean pareil = true;

		if (autrePile == null) {
			return false;
		}

		if (hauteur() != autrePile.hauteur()) {
			return false;
		}

		for (int i = 0; i < hauteur() && pareil; i++) {
			pareil = _contenu[i].equals(autrePile._contenu[i]);
		}

		return pareil;
	}
}