001package components.queue;
002
003import components.standard.Standard;
004
005/**
006 * First-in-first-out (FIFO) queue kernel component with primary methods. (Note:
007 * by package-wide convention, all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code QueueKernel} entries
011 * @mathmodel type QueueKernel 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 QueueKernel<T> extends Standard<Queue<T>>, Iterable<T> {
020
021    /**
022     * Adds {@code x} to the end 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 = #this * <x>}
029     */
030    void enqueue(T x);
031
032    /**
033     * Removes and returns the entry at the front of {@code this}.
034     *
035     * @return the entry removed
036     * @updates this
037     * @requires {@code this /= <>}
038     * @ensures {@code #this = <dequeue> * this}
039     */
040    T dequeue();
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}