001package components.naturalnumber;
002
003/**
004 * {@code NaturalNumberKernel} enhanced with secondary methods.
005 */
006public interface NaturalNumber extends Comparable<NaturalNumber>, NaturalNumberKernel {
007
008    /**
009     * Sets the value of {@code this} to {@code i}, when {@code i} is
010     * non-negative.
011     *
012     * @param i
013     *            the new value
014     * @replaces this
015     * @requires i >= 0
016     * @ensures this = i
017     */
018    void setFromInt(int i);
019
020    /**
021     * Reports whether {@code this} is small enough to convert to {@code int}.
022     *
023     * @return true iff {@code this} is small enough
024     * @ensures {@code canConvertToInt = (this <= Integer.MAX_VALUE)}
025     */
026    boolean canConvertToInt();
027
028    /**
029     * Reports the value of {@code this} as an {@code int}, when {@code this} is
030     * small enough.
031     *
032     * @return the value
033     * @requires {@code this <= Integer.MAX_VALUE}
034     * @ensures toInt = this
035     */
036    int toInt();
037
038    /**
039     * Reports whether {@code s} is of the right form to convert to a
040     * {@code NaturalNumber}. Note that this is an instance method and needs to
041     * be called with a distinguished argument even though the corresponding
042     * parameter ({@code this}) is not going to be used. This method should be a
043     * static method but currently in Java static methods cannot be declared in
044     * interfaces.
045     *
046     * @param s
047     *            the {@code String} to be converted
048     * @return true iff {@code s} is of the right form
049     * @ensures <pre>
050     * canConvertToNatural = there exists n: NATURAL (s = TO_STRING(n))
051     * </pre>
052     */
053    boolean canSetFromString(String s);
054
055    /**
056     * Sets the value of {@code this} to the number whose standard decimal
057     * representation as a {@code String} is {@code s}, when {@code s} has the
058     * appropriate form (i.e., {@code s} is the result of the function
059     * {@code toString} for some {@code NaturalNumber}).
060     *
061     * @param s
062     *            the {@code String} to be converted
063     * @replaces this
064     * @requires there exists n: NATURAL (s = TO_STRING(n))
065     * @ensures s = TO_STRING(this)
066     */
067    void setFromString(String s);
068
069    /**
070     * Copies {@code n} to {@code this}.
071     *
072     * @param n
073     *            {@code NaturalNumber} to copy from
074     * @replaces this
075     * @ensures this = n
076     */
077    void copyFrom(NaturalNumber n);
078
079    /**
080     * Increments {@code this}.
081     *
082     * @updates this
083     * @ensures this = #this + 1
084     */
085    void increment();
086
087    /**
088     * Decrements {@code this}.
089     *
090     * @updates this
091     * @requires this > 0
092     * @ensures this = #this - 1
093     */
094    void decrement();
095
096    /**
097     * Adds {@code n} to {@code this}.
098     *
099     * @param n
100     *            {@code NaturalNumber} to add
101     * @updates this
102     * @ensures this = #this + n
103     */
104    void add(NaturalNumber n);
105
106    /**
107     * Subtracts {@code n} from {@code this}.
108     *
109     * @param n
110     *            {@code NaturalNumber} to subtract
111     * @updates this
112     * @requires this >= n
113     * @ensures this = #this - n
114     */
115    void subtract(NaturalNumber n);
116
117    /**
118     * Multiplies {@code this} by {@code n}.
119     *
120     * @param n
121     *            {@code NaturalNumber} to multiply by
122     * @updates this
123     * @ensures this = #this * n
124     */
125    void multiply(NaturalNumber n);
126
127    /**
128     * Divides {@code this} by {@code n}, returning the remainder.
129     *
130     * @param n
131     *            {@code NaturalNumber} to divide by
132     * @return remainder after division
133     * @updates this
134     * @requires n > 0
135     * @ensures {@code
136     * #this = this * n + divide  and
137     * 0 <= divide < n
138     * }
139     */
140    NaturalNumber divide(NaturalNumber n);
141
142    /**
143     * Raises {@code this} to the power {@code p}.
144     *
145     * @param p
146     *            power to raise to
147     * @updates this
148     * @requires p >= 0
149     * @ensures this = #this ^ (p)
150     */
151    void power(int p);
152
153    /**
154     * Updates {@code this} to the {@code r}-th root of its incoming value.
155     *
156     * @param r
157     *            root
158     * @updates this
159     * @requires r >= 2
160     * @ensures {@code this ^ (r) <= #this < (this + 1) ^ (r)}
161     */
162    void root(int r);
163
164}