//package stack;

/**
 * pb du final/nested
 * inner class : ref ok ?
 * tests annexes ds Datacopy ?
 */

/** A stack of bounded size.
 * @author M. Nebut
 * 01/05
 */
public class BoundedStack {

    /*** Implementation array of the stack. */
    private Object[] array;

    /** Max number of objects in the stack. */
    private int maxNb;

    /** Current number of objects in the stack. */
    private int objNb;

    /** Create an empty stack of max capacity <tt>t</tt>.
     * @param t max number of elements in the stack.
     */
    public BoundedStack(int t) {
	if ( t <= 0 )
	    throw new IllegalArgumentException("Le capa doit être sup à 0, capa = " + t);

	this.array = new Object[t];
	this.maxNb = t;
	this.objNb = 0;

	assert this.isEmpty()
	    && this.maxNb == t
	    && this.array != null
	    : "Etat incohérent";

	assert invariant();
    }

    /** Check class invariant
     */
    private boolean invariant()
    {
	return objNb <= maxNb
	    && objNb >= 0;
    }


    /** Is this stack empty ?
     * @return true if this stack is empty.
     */
    public boolean isEmpty() {
	assert invariant();
	boolean res = (this.objNb == 0);

	assert res == (getObjNumber() == 0);
	assert invariant();

	return res;
    }

    /** Is this stack full ?
     * @return true if this stack is full.
     */
    public boolean isFull() {
	assert invariant();
	boolean res = (this.objNb == this.maxNb);

	assert res == (getObjNumber() == this.maxNb);
	assert invariant();

	return res;
    }

    /** Pushes the object <tt>o</tt> onto this stack.
     * @param o the object to be stacked. 
     */
    public void push(Object o) {
	assert invariant() : "Nombre d'objets dans la pile incohérent";
	assert ! isFull() : "Pile pleine";

	class DataCopy 
	{
	    private int objNbCopy;
	    private Object oRef;

	    DataCopy(Object o)
	    {
		objNbCopy = objNb;
		oRef = o;
	    }

	    boolean isConsistent()
	    {
		return (objNbCopy+1) == objNb
		    && top().equals(oRef);
	    }
	}
	DataCopy copy = null;

	assert ((copy = new DataCopy(o)) != null);


	this.array[this.objNb] = o;
	this.objNb ++;


	assert copy.isConsistent() : "Pb de cohérence";
	assert invariant();
    }

    /** Returns the object on the top of this stack.
     * @return the object on top of this stack.
     */
    public Object top() {
	assert invariant() : "Nombre d'objets dans la pile incohérent";
	assert ! isEmpty() : "Pile vide";

	Object res = this.array[this.objNb-1];

	assert res != null : "Objet retourné vide.";
	assert invariant();

	return res;
    }

    /** Suppresses the object on the top of this stack and returns it.
     * @return the object on top of this stack.
     */
    public Object pop() {
	assert invariant() : "Nombre d'objets dans la pile incohérent";
	assert ! isEmpty() : "Pile vide";

	class DataCopy 
	{
	    private int objNbCopy;
	    private Object topRef;

	    DataCopy(Object top)
	    {
		objNbCopy = objNb;
		topRef = top;
	    }

	    boolean isConsistent(Object res)
	    {
		return (objNbCopy-1) == objNb
		    && topRef.equals(res)
		    && res != null;
	    }
	}
	DataCopy copy = null;

	assert ((copy = new DataCopy(top())) != null);

	this.objNb--;
	
	Object res = this.array[this.objNb];

	assert copy.isConsistent(res) : "Pb de cohérence";
	assert invariant();

	return res;
    }

    /** Returns the number of objects in this stack.
     * @return the number of objects in this stack.
     */
    public int getObjNumber() {
	assert invariant() : "Nombre d'objets dans la pile incohérent";

	return this.objNb;
    }
    
    public String toString() {
	String res="";
	for (int i = 0; i < this.objNb; i++)
	    res += "[" + this.array[i] + "]";
	return res;
    }
    
    public static void main (String[] arg) {

    BoundedStack p = new BoundedStack(3);
    System.out.println(p.toString());
    p.push("un");
    System.out.println(p.top());
    p.push("deux");
    System.out.println(p.top());
    p.push("trois");
    System.out.println(p.top());
    System.out.println(p.toString());
    p.pop();
    System.out.println(p.top());
    p.pop();
    System.out.println(p.top());
    p.pop();
    System.out.println(p.toString());

    }


}