001package components.sortingmachine;
002
003import java.util.Comparator;
004
005import components.standard.Standard;
006
007/**
008 * Sorting machine kernel component with primary methods. (Note: by package-wide
009 * convention, all references are non-null.)
010 *
011 * @param <T>
012 *            type of {@code SortingMachineKernel} entries
013 * @mathdefinitions <pre>
014 * IS_TOTAL_PREORDER (
015 *   r: binary relation on T
016 *  ) : boolean is
017 *  for all x, y, z: T
018 *   ((r(x, y) or r(y, x))  and
019 *    (if (r(x, y) and r(y, z)) then r(x, z)))
020 * </pre>
021 * @mathsubtypes <pre>
022 * SORTING_MACHINE_MODEL is (
023 *   insertion_mode: boolean,
024 *   ordering: binary relation on T,
025 *   contents: finite multiset of T
026 *  )
027 *  exemplar m
028 *  constraint
029 *   IS_TOTAL_PREORDER(m.ordering)
030 * </pre>
031 * @mathmodel type SortingMachineKernel is modeled by SORTING_MACHINE_MODEL
032 * @initially {@code <pre>
033 * (Comparator<T> order):
034 *  aliases reference {@code order}
035 *  requires
036 *   IS_TOTAL_PREORDER(order)
037 *  ensures
038 *   this = (true, order, {})
039 * </pre>  }
040 * @iterator multiset_entries(~this.seen * ~this.unseen) = this.contents
041 */
042public interface SortingMachineKernel<T>
043        extends Standard<SortingMachine<T>>, Iterable<T> {
044
045    /**
046     * Adds {@code x} to the contents of {@code this}.
047     *
048     * @param x
049     *            the element to be added
050     * @aliases reference {@code x}
051     * @updates this.contents
052     * @requires this.insertion_mode
053     * @ensures this.contents = #this.contents union {x}
054     */
055    void add(T x);
056
057    /**
058     * Changes the mode of {@code this} from insertion to extraction.
059     *
060     * @updates this.insertion_mode
061     * @requires this.insertion_mode
062     * @ensures not this.insertion_mode
063     */
064    void changeToExtractionMode();
065
066    /**
067     * Removes and returns some "first" ("smallest") entry from the contents of
068     * {@code this}.
069     *
070     * @return the entry removed
071     * @updates this.contents
072     * @requires <pre>
073     * not this.insertion_mode  and
074     * this.contents /= {}
075     * </pre>
076     * @ensures <pre>
077     * removeFirst is in #this.contents  and
078     * for all x: T where (x is in #this.contents)
079     *  (this.ordering(removeFirst, x))  and
080     * this.contents = #this.contents \ {removeFirst}
081     * </pre>
082     */
083    T removeFirst();
084
085    /**
086     * Reports whether {@code this} is in insertion mode.
087     *
088     * @return true iff {@code this} is in insertion mode
089     * @ensures isInInsertionMode = this.insertion_mode
090     */
091    boolean isInInsertionMode();
092
093    /**
094     * Reports {@code Comparator} being used for sorting by {@code this}.
095     *
096     * @return Comparator used for sorting
097     * @aliases reference returned by {@code order}
098     * @ensures <pre>
099     * order = [Comparator used in the constructor call that created this]
100     * </pre>
101     */
102    Comparator<T> order();
103
104    /**
105     * Reports the number of entries in {@code this}.
106     *
107     * @return the (multiset) size of {@code this.contents}
108     * @ensures size = |this.contents|
109     */
110    int size();
111
112}