001package components.list;
002
003/**
004 * {@code ListKernel} enhanced with secondary methods.
005 *
006 * @param <T>
007 *            type of {@code List} entries
008 */
009public interface List<T> extends ListKernel<T> {
010
011    /**
012     * Reports the front of {@code this.right}.
013     *
014     * @return the front entry of {@code this.right}
015     * @aliases reference returned by {@code rightFront}
016     * @requires {@code this.right /= <>}
017     * @ensures {@code <rightFront> is prefix of this.right}
018     */
019    T rightFront();
020
021    /**
022     * Replaces the entry at the front of {@code this.right} with {@code x}, and
023     * returns the old entry.
024     *
025     * @param x
026     *            the new entry
027     * @return the old front entry of {@code this.right}
028     * @aliases reference {@code x}
029     * @updates this.right
030     * @requires {@code this.right /= <>}
031     * @ensures {@code
032     * <replaceRightFront> is prefix of #this.right  and
033     * this.right = <x> * #this.right[1, |#this.right|)
034     * }
035     */
036    T replaceRightFront(T x);
037
038    /**
039     * Moves the position in {@code this} to the end.
040     *
041     * @updates this
042     * @ensures this.left = #this.left * #this.right and |this.right| = 0
043     */
044    void moveToFinish();
045
046    /**
047     * Retreats the position in {@code this} by one.
048     *
049     * @updates this
050     * @requires {@code this.left /= <>}
051     * @ensures <pre>
052     * this.left * this.right = #this.left * #this.right  and
053     * |this.left| = |#this.left| - 1
054     * </pre>
055     */
056    void retreat();
057
058    /**
059     * Swaps the right strings of {@code this} and {@code list}.
060     *
061     * @param list
062     *            the {@code List} whose right string is to be swapped with the
063     *            right string of {@code this}
064     * @updates this.right, list.right
065     * @ensures <pre>
066     * this.left = #this.left  and  list.left = #list.left  and
067     * this.right = #list.right  and  list.right = #this.right
068     * </pre>
069     */
070    void swapRights(List<T> list);
071
072}