Package components.naturalnumber

Interface NaturalNumberKernel

All Superinterfaces:
Standard<NaturalNumber>
All Known Subinterfaces:
NaturalNumber
All Known Implementing Classes:
NaturalNumber1L, NaturalNumber2, NaturalNumber3, NaturalNumber4, NaturalNumberSecondary
public interface NaturalNumberKernel extends Standard<NaturalNumber>
Natural number kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Subtypes:
NATURAL is integer
 exemplar n
 constraint n >= 0
Mathematical Model (abstract value and abstract invariant of this):
type NaturalNumberKernel is modeled by NATURAL
Constructor(s) (initial abstract value(s) of this):
():
 ensures
  this = 0
(int i):
 requires
  i >= 0
 ensures
  this = i
(String s):
 requires
  there exists n: NATURAL (s = TO_STRING(n))
 ensures
  s = TO_STRING(this)
(NaturalNumber n):
 ensures
  this = n

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    static final int
    RADIX
    A constant, with value 10, holding the radix (or base) for NaturalNumber.

  • Method Summary

    Modifier and Type
    Method
    Description
    int
    divideBy10()
    Divides this by 10 and reports the remainder.
    boolean
    isZero()
    Reports whether this is zero.
    void
    multiplyBy10(int k)
    Multiplies this by 10 and adds k.

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom

  • Field Details

    • RADIX

      static final int RADIX
      A constant, with value 10, holding the radix (or base) for NaturalNumber.
      See Also:

  • Method Details

    • multiplyBy10

      void multiplyBy10(int k)
      Multiplies this by 10 and adds k.
      Parameters:
      k - the int to be added
      Updates:
      this
      Requires:
      0 <= k < 10
      Ensures:
      this = 10 * #this + k

    • divideBy10

      int divideBy10()
      Divides this by 10 and reports the remainder.
      Returns:
      the remainder
      Updates:
      this
      Ensures:
      #this = 10 * this + divideBy10  and
0 <= divideBy10 < 10

    • isZero

      boolean isZero()
      Reports whether this is zero.
      Returns:
      true iff this is zero
      Ensures:
      isZero = (this = 0)