Interface NaturalNumber

All Superinterfaces:
Comparable<NaturalNumber>, NaturalNumberKernel, Standard<NaturalNumber>
All Known Implementing Classes:
NaturalNumber1L, NaturalNumber2, NaturalNumber3, NaturalNumber4, NaturalNumberSecondary

NaturalNumberKernel enhanced with secondary methods.
  • Method Details

    • setFromInt

      void setFromInt(int i)
      Sets the value of this to i, when i is non-negative.
      Parameters:
      i - the new value
      Replaces:
      this
      Requires:
      i >= 0
      Ensures:
      this = i
    • canConvertToInt

      boolean canConvertToInt()
      Reports whether this is small enough to convert to int.
      Returns:
      true iff this is small enough
      Ensures:
      canConvertToInt = (this <= Integer.MAX_VALUE)
    • toInt

      int toInt()
      Reports the value of this as an int, when this is small enough.
      Returns:
      the value
      Requires:
      this <= Integer.MAX_VALUE
      Ensures:
      toInt = this
    • canSetFromString

      Reports whether s is of the right form to convert to a NaturalNumber. Note that this is an instance method and needs to be called with a distinguished argument even though the corresponding parameter (this) is not going to be used. This method should be a static method but currently in Java static methods cannot be declared in interfaces.
      Parameters:
      s - the String to be converted
      Returns:
      true iff s is of the right form
      Ensures:
      canConvertToNatural = there exists n: NATURAL (s = TO_STRING(n))
    • setFromString

      Sets the value of this to the number whose standard decimal representation as a String is s, when s has the appropriate form (i.e., s is the result of the function toString for some NaturalNumber).
      Parameters:
      s - the String to be converted
      Replaces:
      this
      Requires:
      there exists n: NATURAL (s = TO_STRING(n))
      Ensures:
      s = TO_STRING(this)
    • copyFrom

      Copies n to this.
      Parameters:
      n - NaturalNumber to copy from
      Replaces:
      this
      Ensures:
      this = n
    • increment

      void increment()
      Increments this.
      Updates:
      this
      Ensures:
      this = #this + 1
    • decrement

      void decrement()
      Decrements this.
      Updates:
      this
      Requires:
      this > 0
      Ensures:
      this = #this - 1
    • add

      void add(NaturalNumber n)
      Adds n to this.
      Parameters:
      n - NaturalNumber to add
      Updates:
      this
      Ensures:
      this = #this + n
    • subtract

      Subtracts n from this.
      Parameters:
      n - NaturalNumber to subtract
      Updates:
      this
      Requires:
      this >= n
      Ensures:
      this = #this - n
    • multiply

      Multiplies this by n.
      Parameters:
      n - NaturalNumber to multiply by
      Updates:
      this
      Ensures:
      this = #this * n
    • divide

      Divides this by n, returning the remainder.
      Parameters:
      n - NaturalNumber to divide by
      Returns:
      remainder after division
      Updates:
      this
      Requires:
      n > 0
      Ensures:
      #this = this * n + divide  and
      0 <= divide < n
      
    • power

      void power(int p)
      Raises this to the power p.
      Parameters:
      p - power to raise to
      Updates:
      this
      Requires:
      p >= 0
      Ensures:
      this = #this ^ (p)
    • root

      void root(int r)
      Updates this to the r-th root of its incoming value.
      Parameters:
      r - root
      Updates:
      this
      Requires:
      r >= 2
      Ensures:
      this ^ (r) <= #this < (this + 1) ^ (r)