001package components.list;
002
003import components.standard.Standard;
004
005/**
006 * List kernel component with primary methods. (Note: by package-wide
007 * convention, all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code ListKernel} entries
011 * @mathsubtypes <pre>
012 * LIST_MODEL is (
013 *   left: string of T,
014 *   right: string of T
015 *  )
016 * </pre>
017 * @mathmodel type ListKernel is modeled by LIST_MODEL
018 * @initially {@code
019 * ():
020 *  ensures
021 *   this = (<>, <>)
022 * }
023 * @iterator ~this.seen * ~this.unseen = this.left * this.right
024 */
025public interface ListKernel<T> extends Standard<List<T>>, Iterable<T> {
026
027    /**
028     * Adds {@code x} to the beginning of {@code this.right}.
029     *
030     * @param x
031     *            the entry to be added
032     * @aliases reference {@code x}
033     * @updates this.right
034     * @ensures {@code this.right = <x> * #this.right}
035     */
036    void addRightFront(T x);
037
038    /**
039     * Removes and returns the entry at the front of {@code this.right}.
040     *
041     * @return the front entry of {@code this.right}
042     * @updates this.right
043     * @requires {@code this.right /= <>}
044     * @ensures {@code #this.right = <removeRightFront> * this.right}
045     */
046    T removeRightFront();
047
048    /**
049     * Advances the position in {@code this} by one.
050     *
051     * @updates this
052     * @requires {@code this.right /= <>}
053     * @ensures <pre>
054     * this.left * this.right = #this.left * #this.right  and
055     * |this.left| = |#this.left| + 1
056     * </pre>
057     */
058    void advance();
059
060    /**
061     * Moves the position in {@code this} to the beginning.
062     *
063     * @updates this
064     * @ensures this.right = #this.left * #this.right and |this.left| = 0
065     */
066    void moveToStart();
067
068    /**
069     * Reports length of {@code this.left}.
070     *
071     * @return the length of {@code this.left}
072     * @ensures leftLength = |this.left|
073     */
074    int leftLength();
075
076    /**
077     * Reports length of {@code this.right}.
078     *
079     * @return the length of {@code this.right}
080     * @ensures rightLength = |this.right|
081     */
082    int rightLength();
083
084}