001package components.standard;
002
003/**
004 * Interface for {@code newInstance}, {@code clear}, and {@code transferFrom}
005 * methods that are expected of every mutable type in the "components" type
006 * families.
007 *
008 * Each of the {@code Standard} methods results in some variable having "an
009 * initial value" of its type. The meaning of this phrase, indeed the meaning of
010 * the "clears" parameter mode in all contracts in the "components" type
011 * families, is as follows. If the type {@code T} has a no-argument constructor,
012 * then the initial value satisfies the contract of the no-argument constructor.
013 * If the type does not have a no-argument constructor, then the initial value
014 * satisfies the contract of the constructor call that was used to initialize
015 * the variable whose old value is relevant in the contract of the method.
016 *
017 * @param <T>
018 *            type with these methods
019 */
020public interface Standard<T> {
021
022    /**
023     * Returns a new object with the same <i>dynamic</i> type as {@code this},
024     * having an initial value.
025     *
026     * If the type {@code T} has a no-argument constructor, then the value of
027     * the new returned object satisfies the contract of the no-argument
028     * constructor for {@code T}. If {@code T} does not have a no-argument
029     * constructor, then the value of the new returned object satisfies the
030     * contract of the constructor call that was used to initialize {@code this}
031     * .
032     *
033     * @return new object "like" {@code this} with an initial value
034     * @ensures is_initial(newInstance)
035     */
036    T newInstance();
037
038    /**
039     * Resets {@code this} to an initial value.
040     *
041     * If the type {@code T} has a no-argument constructor, then {@code this}
042     * satisfies the contract of the no-argument constructor for {@code T}. If
043     * {@code T} does not have a no-argument constructor, then {@code this}
044     * satisfies the contract of the constructor call that was used to
045     * initialize {@code #this}.
046     *
047     * @clears this
048     */
049    void clear();
050
051    /**
052     * Sets {@code this} to the incoming value of {@code source}, and resets
053     * {@code source} to an initial value; the declaration notwithstanding, the
054     * <i>dynamic</i> type of {@code source} must be the same as the
055     * <i>dynamic</i> type of {@code this}.
056     *
057     * If the type {@code T} has a no-argument constructor, then {@code source}
058     * satisfies the contract of the no-argument constructor for {@code T}. If
059     * {@code T} does not have a no-argument constructor, then {@code source}
060     * satisfies the contract of the constructor call that was used to
061     * initialize {@code #source}.
062     *
063     * @param source
064     *            object whose value is to be transferred
065     * @replaces this
066     * @clears source
067     * @ensures this = #source
068     */
069    void transferFrom(T source);
070
071}