001package components.stack;
002
003import components.standard.Standard;
004
005/**
006 * Last-in-first-out (LIFO) stack kernel component with primary methods. (Note:
007 * by package-wide convention, all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code StackKernel} entries
011 * @mathmodel type StackKernel is modeled by string of T
012 * @initially {@code
013 * ():
014 *  ensures
015 *   this = <>
016 * }
017 * @iterator ~this.seen * ~this.unseen = this
018 */
019public interface StackKernel<T> extends Standard<Stack<T>>, Iterable<T> {
020
021    /**
022     * Adds {@code x} to the top of {@code this}.
023     *
024     * @param x
025     *            the entry to be added
026     * @aliases reference {@code x}
027     * @updates this
028     * @ensures {@code this = <x> * #this}
029     */
030    void push(T x);
031
032    /**
033     * Removes and returns the entry at the top of {@code this}.
034     *
035     * @return the entry removed
036     * @updates this
037     * @requires {@code this /= <>}
038     * @ensures {@code #this = <pop> * this}
039     */
040    T pop();
041
042    /**
043     * Reports length of {@code this}.
044     *
045     * @return the length of {@code this}
046     * @ensures length = |this|
047     */
048    int length();
049
050}