/**
 * A simple implementation of the ADT Stack 
 * @jass.invariant <b>range</b>: <code>-1&lt;=top&amp;&amp;top&lt;storage.length</code>; <br><b>valid_content</b>: <code>storage.length==0||(forall i : {0..top} storage[i]!=null)</code>; <br><b>LIFO</b>: <code>isFull()||push("neco").pop().equals("neco")</code>
 */
public class Stack implements Cloneable {

    /**
     * positions where to store next element
     */
    protected int top = -1;

    /**
     * the internal storage
     */
    protected Object[] storage;

    /** 
     * create an empty Stack with capacity
     * @jass.require <code>capacity&gt;0</code>
     * @jass.ensure <b>empty_after_creation</b>: <code>isEmpty()</code>
     */
    public Stack(int capacity) {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(capacity)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "Stack(int)", true), jassParameters);


    	/* precondition */
    	if (!(capacity>0)) throw new jass.runtime.PreconditionException("Stack","Stack(int)",20,null);
	storage = new Object[capacity];
    	/* postcondition */
    	if (!(jassInternal_isEmpty())) throw new jass.runtime.PostconditionException("Stack","Stack(int)",22,"empty_after_creation");
    	/* invariant */
    	jassCheckInvariant("at end of method Stack(int).");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "Stack(int)", false), jassParameters);

    }

    /**
     * is the stack empty?
     * @jass.ensure <b>changeonly</b> { }; <br>

     */
    public boolean isEmpty() {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "isEmpty()", true), jassParameters);
    	boolean jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method isEmpty().");
    	Stack jassOld = (Stack)this.clone();
    	jassResult = ( top < 0);
    	/* postcondition */
    	if (!(top == jassOld.top && jass.runtime.Tool.arrayEquals(storage,jassOld.storage))) throw new jass.runtime.PostconditionException("Stack","isEmpty()",-1,"Method has changed old value.");
    	/* invariant */
    	jassCheckInvariant("before return in method isEmpty().");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "isEmpty()", false), jassParameters);


    	return jassResult;
    }
  
    /**
     * is the stack full?
     * @jass.ensure <b>changeonly</b> { }; <br>

     */
    public boolean isFull() {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "isFull()", true), jassParameters);
    	boolean jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method isFull().");
    	Stack jassOld = (Stack)this.clone();
    	jassResult = ( top == storage.length - 1);
    	/* postcondition */
    	if (!(top == jassOld.top && jass.runtime.Tool.arrayEquals(storage,jassOld.storage))) throw new jass.runtime.PostconditionException("Stack","isFull()",-1,"Method has changed old value.");
    	/* invariant */
    	jassCheckInvariant("before return in method isFull().");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "isFull()", false), jassParameters);


    	return jassResult;    
    }
  
    /**
     * push a real (non-null) object to the stack
     * @jass.require <b>valid_object</b>: <code>o!=null</code>; <br><b>stack_not_full</b>: <code>!isFull()</code>
     * @jass.ensure <b>changeonly</b> {top, storage }; <br>
<b>nonempty_after_push</b>: <code>!isEmpty()</code>; <br><b>push_increments_top</b>: <code>Old.top==top-1</code>
     */
    public Stack push(Object o) {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(o)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "push(java.lang.Object)", true), jassParameters);
    	Stack jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method push(java.lang.Object).");
    	Stack jassOld = (Stack)this.clone();
    	/* precondition */
    	if (!(o!=null)) throw new jass.runtime.PreconditionException("Stack","push(java.lang.Object)",45,"valid_object");
    	if (!(!jassInternal_isFull())) throw new jass.runtime.PreconditionException("Stack","push(java.lang.Object)",45,"stack_not_full");
	top++;
	storage[top] = o;
    	jassResult = ( this);
    	/* postcondition */
    	if (!(!jassInternal_isEmpty())) throw new jass.runtime.PostconditionException("Stack","push(java.lang.Object)",50,"nonempty_after_push");
    	if (!(jassOld.top==top-1)) throw new jass.runtime.PostconditionException("Stack","push(java.lang.Object)",51,"push_increments_top");
    	/* invariant */
    	jassCheckInvariant("before return in method push(java.lang.Object).");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "push(java.lang.Object)", false), jassParameters);


    	return jassResult;
    }
  
    /**
     * take an object from the stack
     * @jass.require <b>stack_not_empty</b>: <code>!isEmpty()</code>
     * @jass.ensure <b>changeonly</b> {top }; <br>
<b>valid_object</b>: <code>Result!=null</code>
     */
    public Object pop() {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "pop()", true), jassParameters);
    	java.lang.Object jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method pop().");
    	Stack jassOld = (Stack)this.clone();
    	/* precondition */
    	if (!(!jassInternal_isEmpty())) throw new jass.runtime.PreconditionException("Stack","pop()",59,"stack_not_empty");
	Object o = storage[top];
	top--;
    	jassResult = ( o);
    	/* postcondition */
    	if (!(jassResult!=null)) throw new jass.runtime.PostconditionException("Stack","pop()",63,"valid_object");
    	if (!(jass.runtime.Tool.arrayEquals(storage,jassOld.storage))) throw new jass.runtime.PostconditionException("Stack","pop()",-1,"Method has changed old value.");
    	/* invariant */
    	jassCheckInvariant("before return in method pop().");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "pop()", false), jassParameters);


    	return jassResult;
    }
  
    /**
     * does the stack contain the object
     * @jass.require <code>o!=null</code>
     * @jass.ensure <b>changeonly</b> { }; <br>

     */
    public boolean contains(Object o) {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(o)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "contains(java.lang.Object)", true), jassParameters);
    	boolean jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method contains(java.lang.Object).");
    	Stack jassOld = (Stack)this.clone();
    	/* precondition */
    	if (!(o!=null)) throw new jass.runtime.PreconditionException("Stack","contains(java.lang.Object)",70,null);
	int i = 0;
    	int jassVariant;
	while (i <= top && !storage[i].equals(o))
	{
		if(!(0<=i&&i<=top+1)) throw new jass.runtime.LoopInvariantException("Stack","contains(java.lang.Object)",73,null);
		jassVariant=top+1-i;
		if(!(jassVariant>=0)) throw new jass.runtime.LoopVariantException("Stack","contains(java.lang.Object)",74,"Loopvariant is below zero.");
	    i++;
		if(!(jassVariant>top+1-i)) throw new jass.runtime.LoopVariantException("Stack","contains(java.lang.Object)",74,"Loopvariant was not decreased.");
	}
	if(!(0<=i&&i<=top+1)) throw new jass.runtime.LoopInvariantException("Stack","contains(java.lang.Object)",73,null);
    	jassResult = ( i <= top);
    	/* postcondition */
    	if (!(top == jassOld.top && jass.runtime.Tool.arrayEquals(storage,jassOld.storage))) throw new jass.runtime.PostconditionException("Stack","contains(java.lang.Object)",-1,"Method has changed old value.");
    	/* invariant */
    	jassCheckInvariant("before return in method contains(java.lang.Object).");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "contains(java.lang.Object)", false), jassParameters);


    	return jassResult;    
    }

    protected Object clone() {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "clone()", true), jassParameters);
    	java.lang.Object jassResult;

    	/* invariant */
    	jassCheckInvariant("at begin of method clone().");
	/* Use the Objects clone method. This is enough cause only top
	   is refered with Old expressions. */
	Object b = null;
	try {
	    b = super.clone();
	}
	catch (CloneNotSupportedException e){}
    	jassResult = ( b);
    	/* invariant */
    	jassCheckInvariant("before return in method clone().");
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(jassResult)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "clone()", false), jassParameters);


    	return jassResult;
    }

	/* --- The following methods of class Stack are generated by JASS --- */

  
    
    public boolean jassInternal_isFull() {
	return top == storage.length - 1;    
    }

  
    
    public Stack jassInternal_push(Object o) {
	top++;
	storage[top] = o;
	return this;
    }

  
    
    public Object jassInternal_pop() {
	Object o = storage[top];
	top--;
	return o;
    }


    
    public boolean jassInternal_isEmpty() {
	return top < 0;
    }

	private void jassCheckInvariant(String msg) {
		if (!(-1<=top&&top<storage.length)) throw new jass.runtime.InvariantException("Stack",null,94,"Exception occured "+msg+" (range)");
		if (!(storage.length==0||(jassCheckForAll_0_Stack()))) throw new jass.runtime.InvariantException("Stack",null,95,"Exception occured "+msg+" (valid_content)");
		if (!(jassInternal_isFull()||jassInternal_push("neco").jassInternal_pop().equals("neco"))) throw new jass.runtime.InvariantException("Stack",null,98,"Exception occured "+msg+" (LIFO)");
	}

	protected final boolean jassCheckForAll_0_Stack() {
		try {
			int i;
			for(i = 0;i <= top;i++) {
				if (!(storage[i]!=null)) return false;
			}
			return true;
		}
		catch (ArrayIndexOutOfBoundsException jassException) {
			throw new jass.runtime.AssertionException("Stack",null,96,"Arraybounds in forall/exists expression violated ! ("+jassException.toString()+")");
		}
	}


	protected void finalize () throws java.lang.Throwable {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "finalize()", true), jassParameters);
		super.finalize();
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "finalize()", false), jassParameters);
	}

	public boolean equals (java.lang.Object par0) {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(par0)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "equals(java.lang.Object)", true), jassParameters);
		boolean returnValue = super.equals(par0);
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(returnValue)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "equals(java.lang.Object)", false), jassParameters);
		return returnValue;
	}

	public java.lang.String toString () {
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jass.runtime.traceAssertion.Parameter[] jassParameters; jassParameters = new jass.runtime.traceAssertion.Parameter[] {}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "toString()", true), jassParameters);
		java.lang.String returnValue = super.toString();
      jass.runtime.traceAssertion.CommunicationManager.internalAction = true; jassParameters = new jass.runtime.traceAssertion.Parameter[] {new jass.runtime.traceAssertion.Parameter(returnValue)}; jass.runtime.traceAssertion.CommunicationManager.internalAction = false; jass.runtime.traceAssertion.CommunicationManager.communicate(this, new jass.runtime.traceAssertion.MethodReference("null", "Stack", "toString()", false), jassParameters);
		return returnValue;
	}
}