001package components.sequence;
002
003import components.standard.Standard;
004
005/**
006 * Sequence kernel component with primary methods. (Note: by package-wide
007 * convention, all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code SequenceKernel} entries
011 *
012 * @mathmodel type SequenceKernel is modeled by string of T
013 * @initially {@code
014 * ():
015 *  ensures
016 *   this = <>
017 * }
018 * @iterator ~this.seen * ~this.unseen = this
019 */
020public interface SequenceKernel<T> extends Standard<Sequence<T>>, Iterable<T> {
021
022    /**
023     * Adds the entry {@code x} at position {@code pos} of {@code this}.
024     *
025     * @param pos
026     *            the position at which to add an entry
027     * @param x
028     *            the entry to be added
029     * @aliases reference {@code x}
030     * @updates this
031     * @requires {@code 0 <= pos and pos <= |this|}
032     * @ensures {@code this = #this[0, pos) * <x> * #this[pos, |#this|)}
033     */
034    void add(int pos, T x);
035
036    /**
037     * Removes and returns the entry at position {@code pos} of {@code this} .
038     *
039     * @param pos
040     *            the position at which to remove an entry
041     * @return the entry removed
042     * @updates this
043     * @requires {@code 0 <= pos and pos < |this|}
044     * @ensures {@code
045     * this = #this[0, pos) * #this[pos+1, |#this|)  and
046     * <remove> = #this[pos, pos+1)
047     * }
048     */
049    T remove(int pos);
050
051    /**
052     * Reports the length of {@code this}.
053     *
054     * @return the length
055     * @ensures length = |this|
056     */
057    int length();
058
059}