001package components.naturalnumber;
002
003import components.standard.Standard;
004
005/**
006 * Natural number kernel component with primary methods. (Note: by package-wide
007 * convention, all references are non-null.)
008 *
009 * @mathsubtypes <pre>
010 * NATURAL is integer
011 *  exemplar n
012 *  constraint n >= 0
013 * </pre>
014 * @mathmodel type NaturalNumberKernel is modeled by NATURAL
015 * @initially <pre>
016 * ():
017 *  ensures
018 *   this = 0
019 * (int i):
020 *  requires
021 *   i >= 0
022 *  ensures
023 *   this = i
024 * (String s):
025 *  requires
026 *   there exists n: NATURAL (s = TO_STRING(n))
027 *  ensures
028 *   s = TO_STRING(this)
029 * (NaturalNumber n):
030 *  ensures
031 *   this = n
032 * </pre>
033 */
034public interface NaturalNumberKernel extends Standard<NaturalNumber> {
035
036    /**
037     * A constant, with value 10, holding the radix (or base) for NaturalNumber.
038     */
039    int RADIX = 10;
040
041    /**
042     * Multiplies {@code this} by 10 and adds {@code k}.
043     *
044     * @param k
045     *            the {@code int} to be added
046     * @updates this
047     * @requires {@code 0 <= k < 10}
048     * @ensures this = 10 * #this + k
049     */
050    void multiplyBy10(int k);
051
052    /**
053     * Divides {@code this} by 10 and reports the remainder.
054     *
055     * @return the remainder
056     * @updates this
057     * @ensures {@code
058     * #this = 10 * this + divideBy10  and
059     * 0 <= divideBy10 < 10
060     * }
061     */
062    int divideBy10();
063
064    /**
065     * Reports whether {@code this} is zero.
066     *
067     * @return true iff {@code this} is zero
068     * @ensures isZero = (this = 0)
069     */
070    boolean isZero();
071
072}