/**
 *  Description of the Class
 *
 * @author     Marc Champesme
 * @version    25 novembre 2004
 * @created    17 novembre 2003
 */
public class PileElem implements Cloneable {
	/*@
	  @ invariant estVide() <==> (hauteur() == 0);
	  @ invariant estVide() <==> equals(PILE_VIDE);
	  @*/
	/**
	 *  Remplace le generateur pileVide
	 */
	public final static PileElem PILE_VIDE = new PileElem(0);
	private static int _tailleInitiale = 20;
	private static int _incrementTaille = 10;
	private Elem[] _contenu;
	private int _hauteur;


	/**
	 *  Remplace le generateur pileVide
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public PileElem() {
		this(_tailleInitiale);
	}


	/**
	 *  Remplace le generateur pileVide
	 *
	 * @param  capacite  Description of the Parameter
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public PileElem(int capacite) {
		_contenu = new Elem[capacite];
	}


	/**
	 *  Description of the Method
	 */
	/*@
	  @ requires !estVide();
	  @ ensures hauteur() == \old(hauteur()) - 1;
	  @*/
	public void depiler() {
		_hauteur--;
	}


	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 */
	/*@
	  @ ensures !estVide();
	  @ ensures hauteur() == \old(hauteur()) + 1;
	  @ ensures sommet() == elt;
	  @*/
	public void empiler(Elem elt) {
		if (_contenu.length >= _hauteur) {
			Elem[] nouveauConteneur;
			nouveauConteneur = new Elem[_contenu.length + _incrementTaille];
			for (int i = 0; i < _hauteur; i++) {
				nouveauConteneur[i] = _contenu[i];
			}
			_contenu = nouveauConteneur;
		}
		_contenu[_hauteur] = elt;
		_hauteur++;
	}


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


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


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @
	  @ pure
	  @*/
	public Elem sommet() {
		return _contenu[_hauteur - 1];
	}


	/**
	 *  Teste l'égalité entre l'objet spécifié et cette pile. Renvoie <code>true</code>
	 *  si et seulement si l'objet spécifié est aussi une <code>PileElem</code>,
	 *  que les deux piles ont la m&ecirc;me hauteur et que toutes les paires
	 *  d'éléments correspondants dans les deux listes sont <i>egales</i> (au sens
	 *  de ==). En d'autres termes, deux piles 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 pile.
	 * @return      <code>true</code> si l'objet spécifié est <i>equal </i>
	 *      &agrave; cette pile.
	 */
	/*@
	  @ also
	  @ ensures (this == obj) ==> \result;
	  @ ensures \result
	  @		==> (obj instanceof PileElem
	  @		     && this.hauteur() == ((PileElem)obj).hauteur());
	  @ ensures (obj == null) ==> !\result;
	  @ pure
	  @*/
	public boolean equals(Object obj) {
		if (this == obj) {
			return true;
		}

		if (!(obj instanceof PileElem)) {
			return false;
		}

		PileElem autrePile = (PileElem) obj;

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

		boolean pareil = true;

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

		return pareil;
	}


	/**
	 *  Renvoie une copie de surface de cette instance de <code>PileElem</code>
	 *  (Les éléments eux-m&ecirc;mes ne sont pas copiés).
	 *
	 * @return    un clone de cette instance de <code>PileElem</code> .
	 */
	/*@ also
	  @ ensures \result != null;
	  @ ensures \result != this;
	  @ ensures \result.equals(this);
	  @ ensures \typeof(\result) == \typeof(this);
	  @
	  @ pure
	  @*/
	public Object clone() {
		PileElem leClone;
		try {
			leClone = (PileElem) super.clone();
		} catch (CloneNotSupportedException e) {
			// Impossible car cette classe implemente
			// clone() et Object aussi
			throw new InternalError(e.toString());
		}
		leClone._contenu = new Elem[_hauteur];
		for (int i = 0; i < _hauteur; i++) {
			leClone._contenu[i] = _contenu[i];
		}
		// Inutile de copier la valeur de nbElements car super.clone()
		// l'a déja fait
		//leClone._hauteur = hauteur();
		return leClone;
	}

}