/**
 * Last-in-first-out (LIFO) stack component with integer entries.
 * 
 * @mathmodel <pre>
 * {@code StackOfInteger is modeled by string of integer}
 * </pre>
 * @constraint <pre>
 * {@code [no constraint for this component]}
 * </pre>
 * 
 * @initially <pre>
 *  {@code constructor()
 *    ensures
 *      this = <>
 *
 *  constructor(int initialCapacity)
 *    requires
 *      initialCapacity > 0
 *    ensures
 *      this = <> and
 *      [the underlying representation may preallocate
 *       memory for initialCapacity entries]}
 * </pre>
 * 
 * @author Paolo Bucci
 */
public interface StackOfInteger {

    /**
     * Adds x to the top of {@code this}.
     * 
     * @param x
     *            the entry to be added
     * @alters this
     * @ensures {@code this = <x> * #this}
     */
    void push(int x);

    /**
     * Removes the entry at the top of {@code this}.
     * 
     * @requires {@code this /= <>}
     * @alters this
     * @ensures {@code #this = <pop> * this}
     * @return the entry removed
     */
    int pop();

    /**
     * Reports the entry at the top of {@code this}.
     * 
     * @requires {@code this /= <>}
     * @ensures {@code <top> is prefix of this}
     * @return the top entry of this
     */
    int top();

    /**
     * Reports the length of {@code this}.
     * 
     * @ensures {@code length = |this|}
     * @return the length of {@code this}
     */
    int length();

}