001package components.sequence;
002
003/**
004 * {@code SequenceKernel} enhanced with secondary methods.
005 *
006 * @param <T>
007 *            type of {@code Sequence} entries
008 */
009public interface Sequence<T> extends SequenceKernel<T> {
010
011    /**
012     * Reports the entry at position {@code pos} of {@code this}.
013     *
014     * @param pos
015     *            the position of the entry
016     * @return the entry at that position
017     * @aliases reference returned by {@code entry}
018     * @requires {@code 0 <= pos and pos < |this|}
019     * @ensures {@code <entry> = this[pos, pos+1)}
020     */
021    T entry(int pos);
022
023    /**
024     * Replaces the entry at position {@code pos} of {@code this} with the entry
025     * {@code x} and returns the old entry at that position.
026     *
027     * @param pos
028     *            the position at which to replace an entry
029     * @param x
030     *            the entry replacing the old one
031     * @return the old entry at that position
032     * @aliases reference {@code x}
033     * @updates this
034     * @requires {@code 0 <= pos and pos < |this|}
035     * @ensures {@code
036     * <replaceEntry> = #this[pos, pos+1)  and
037     * this = #this[0, pos) * <x> * #this[pos+1, |#this|)
038     * }
039     */
040    T replaceEntry(int pos, T x);
041
042    /**
043     * Concatenates ("appends") {@code s} to the end of {@code this}.
044     *
045     * @param s
046     *            the {@code Sequence} to be appended
047     * @updates this
048     * @clears s
049     * @ensures this = #this * #s
050     */
051    void append(Sequence<T> s);
052
053    /**
054     * Reverses ("flips") {@code this}.
055     *
056     * @updates this
057     * @ensures this = rev(#this)
058     */
059    void flip();
060
061    /**
062     * Inserts {@code s} into {@code this} at position {@code pos}, i.e., after
063     * the {@code pos}-th entry of {@code this}; and clears {@code s}.
064     *
065     * @param pos
066     *            the position at which to insert
067     * @param s
068     *            the {@code Sequence} to be inserted
069     * @updates this
070     * @clears s
071     * @requires {@code 0 <= pos and pos <= |this|}
072     * @ensures this = #this[0, pos) * #s * #this[pos, |#this|)
073     */
074    void insert(int pos, Sequence<T> s);
075
076    /**
077     * Removes the substring of {@code this} starting at position {@code pos1}
078     * and ending at position {@code pos2-1} and puts in it {@code s}.
079     *
080     * @param pos1
081     *            the position of the first entry that is extracted
082     * @param pos2
083     *            the position of the first entry, after the extracted
084     *            substring, that is not extracted
085     * @param s
086     *            upon return, the extracted substring
087     * @updates this
088     * @replaces s
089     * @requires {@code 0 <= pos1 and pos1 <= pos2 and pos2 <= |this|}
090     * @ensures <pre>
091     * this = #this[0, pos1) * #this[pos2, |#this|)  and
092     * s = #this[pos1, pos2)
093     * </pre>
094     */
095    void extract(int pos1, int pos2, Sequence<T> s);
096
097}