001package components.stack;
002
003/**
004 * {@code StackKernel} enhanced with secondary methods.
005 *
006 * @param <T>
007 *            type of {@code Stack} entries
008 */
009public interface Stack<T> extends StackKernel<T> {
010
011    /**
012     * Reports the top of {@code this}.
013     *
014     * @return the top entry of {@code this}
015     * @aliases reference returned by {@code top}
016     * @requires {@code this /= <>}
017     * @ensures {@code <top> is prefix of this}
018     */
019    T top();
020
021    /**
022     * Replaces the top of {@code this} with {@code x}, and returns the old top.
023     *
024     * @param x
025     *            the new top entry
026     * @return the old top entry
027     * @aliases reference {@code x}
028     * @updates this
029     * @requires {@code this /= <>}
030     * @ensures {@code
031     * <replaceTop> is prefix of #this  and
032     * this = <x> * #this[1, |#this|)
033     * }
034     */
035    T replaceTop(T x);
036
037    /**
038     * Reverses ("flips") {@code this}.
039     *
040     * @updates this
041     * @ensures this = rev(#this)
042     */
043    void flip();
044
045}