001package components.set;
002
003import components.standard.Standard;
004
005/**
006 * Set kernel component with primary methods. (Note: by package-wide convention,
007 * all references are non-null.)
008 *
009 * @param <T>
010 *            type of {@code SetKernel} elements
011 * @mathmodel type SetKernel is modeled by finite set of T
012 * @initially <pre>
013 * ():
014 *  ensures
015 *   this = {}
016 * </pre>
017 * @iterator <pre>
018 * entries(~this.seen * ~this.unseen) = this  and
019 * |~this.seen * ~this.unseen| = |this|
020 * </pre>
021 */
022public interface SetKernel<T> extends Standard<Set<T>>, Iterable<T> {
023
024    /**
025     * Adds {@code x} to this.
026     *
027     * @param x
028     *            the element to be added
029     * @aliases reference {@code x}
030     * @updates this
031     * @requires x is not in this
032     * @ensures this = #this union {x}
033     */
034    void add(T x);
035
036    /**
037     * Removes {@code x} from this, and returns it.
038     *
039     * @param x
040     *            the element to be removed
041     * @return the element removed
042     * @updates this
043     * @requires x is in this
044     * @ensures <pre>
045     * this = #this \ {x}  and
046     * remove = x
047     * </pre>
048     */
049    T remove(T x);
050
051    /**
052     * Removes and returns an arbitrary element from {@code this}.
053     *
054     * @return the element removed from {@code this}
055     * @updates this
056     * @requires |this| > 0
057     * @ensures <pre>
058     * removeAny is in #this and
059     * this = #this \ {removeAny}
060     * </pre>
061     */
062    T removeAny();
063
064    /**
065     * Reports whether {@code x} is in {@code this}.
066     *
067     * @param x
068     *            the element to be checked
069     * @return true iff element is in {@code this}
070     * @ensures contains = (x is in this)
071     */
072    boolean contains(T x);
073
074    /**
075     * Reports size (cardinality) of {@code this}.
076     *
077     * @return the number of elements in {@code this}
078     * @ensures size = |this|
079     */
080    int size();
081
082}