class BIG_INTEGER_NUMBER

Features exported to INTEGER_GENERAL_NUMBER

To implement NUMBER (do not use this class, see NUMBER).

Direct parents

conformant parents

INTEGER_GENERAL_NUMBER

Summary

creation features

exported features

Misc:

Multiplication

division

Implementation:

comparisons with NUMBER

comparisons with REAL_64

Implementation:

Binary operators for two NUMBERs:

Unary operators for two NUMBERs:

To know more about a NUMBER:

Conversions and printing:

To mimic NUMERIC:

To mix NUMBER and INTEGER_64:

Misc:

Implementation:

To implement efficient calculus

Details

from_native_array (na: NATIVE_ARRAY [E_][INTEGER], cap: INTEGER, neg: BOOLEAN)

require

    ensure

      is_positive: BOOLEAN

      Is Current > 0 ?

      ensure

      • Result = Current @> 0

      is_negative: BOOLEAN

      Is Current < 0 ?

      ensure

      • Result = Current @< 0

      \\ (other: NUMBER): NUMBER

      Remainder of division of Current by other.

      require

      • is_integer_general_number
      • other.is_integer_general_number
      • divisible(other)

      ensure

      • Result.is_integer_general_number
      • not Result.is_negative and Result < other.abs

      @\\ (other: INTEGER_64): NUMBER

      Remainder of division of Current by other.

      require

      • is_integer_general_number
      • other /= 0

      ensure

      • Result.is_integer_general_number

      hash_code: INTEGER

      The hash-code value of Current.

      ensure

      • good_hash_value: Result >= 0

      gcd (other: NUMBER): INTEGER_GENERAL_NUMBER

      Great Common Divisor of Current and other.

      require

      • other.is_integer_general_number
      • is_integer_general_number

      ensure

      • not Result.is_negative
      • Result.is_zero implies Current.is_zero and other.is_zero
      • not Result.is_zero implies (Current / Result).gcd(other / Result).is_one

      is_integer_value: BOOLEAN
      force_to_real_64: REAL

      Conversion of Current in a REAL_64.

      require

      • fit_real

      -: NUMBER

      Opposite of Current.

      ensure

      • Result /= Void

      + (other: NUMBER): NUMBER

      Sum of Current and other.

      require

      • other /= Void

      ensure

      • (Result - other).is_equal(Current)

      // (other: NUMBER): NUMBER

      Divide Current by other (Integer division).

      require

      • is_integer_general_number
      • other.is_integer_general_number
      • divisible(other)

      ensure

      • Result.is_integer_general_number
      • Current.is_equal(Result * other + Current \\ other)

      @// (other: INTEGER_64): NUMBER

      Divide Current by other (Integer division).

      require

      • is_integer_general_number
      • other /= 0

      ensure

      • Result.is_integer_general_number

      * (other: NUMBER): NUMBER

      Product of Current and other.

      require

      • other /= Void

      ensure

      • Result /= Void

      @/ (other: INTEGER_64): NUMBER

      Quotient of Current and other.

      require

      • other /= 0

      ensure

      • Result /= Void

      @+ (other: INTEGER_64): NUMBER

      Sum of Current and other.

      ensure

      • Result /= Void

      @* (other: INTEGER_64): NUMBER

      ensure

      • Result /= Void

      add_with_big_integer_number (other: BIG_INTEGER_NUMBER): NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      add_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      multiply_with_big_integer_number (other: BIG_INTEGER_NUMBER): NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      multiply_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      integer_divide_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      remainder_of_divide_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      integer_divide_big_integer_number (other: BIG_INTEGER_NUMBER): INTEGER_GENERAL_NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      remainder_of_divide_big_integer_number (other: BIG_INTEGER_NUMBER): INTEGER_GENERAL_NUMBER

      require

      • other /= Void

      ensure

      • Result /= Void

      gcd_with_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER

      require

      • other /= Void

      inverse: NUMBER

      require

      • divisible(Current)

      ensure

      • Result /= Void

      @= (other: INTEGER_64): BOOLEAN

      Is Current equal other ?

      @< (other: INTEGER_64): BOOLEAN

      Is Current strictly less than other?

      ensure

      • Result = not (Current @>= other)

      @> (other: INTEGER_64): BOOLEAN

      Is Current strictly greater than other?

      ensure

      • Result = not (Current @<= other)

      @>= (other: INTEGER_64): BOOLEAN

      Is Current greater or equal than other?

      ensure

      • Result = not (Current @< other)

      @<= (other: INTEGER_64): BOOLEAN

      Is Current less or equal other?

      ensure

      • Result = not (Current @> other)

      < (other: NUMBER): BOOLEAN

      Is Current strictly less than other?

      require

      • other_exists: other /= Void

      ensure

      • asymmetric: Result implies not (other < Current)

      #= (other: REAL): BOOLEAN

      Is Current equal other?

      #< (other: REAL): BOOLEAN

      Is Current strictly less than other?

      ensure

      • Result implies not (Current #>= other)

      #<= (other: REAL): BOOLEAN

      Is Current less or equal other?

      ensure

      • Result = not (Current #> other)

      #> (other: REAL): BOOLEAN

      Is Current strictly greater than other?

      ensure

      • Result = not (Current #<= other)

      #>= (other: REAL): BOOLEAN

      Is Current greater or equal than other?

      ensure

      • Result = not (Current #< other)

      greater_with_big_integer_number (other: BIG_INTEGER_NUMBER): BOOLEAN

      require

      • other /= Void

      greater_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): BOOLEAN

      require

      • other /= Void

      is_zero: BOOLEAN

      Is it 0 ?

      ensure

      • Result = Current @= 0

      is_one: BOOLEAN

      Is it 1 ?

      ensure

      • Result = Current @= 1

      is_equal (other: NUMBER): BOOLEAN

      Compares two LARGE_INTEGERs. As they both have same sign comparison is done with absolute values.

      require

      • other /= Void

      ensure

      • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
      • trichotomy: Result = (not (Current < other) and not (other < Current))
      • Result implies hash_code = other.hash_code

      append_in (buffer: STRING)

      Append the equivalent of to_string at the end of buffer. Thus you can save memory because no other STRING is allocated for the job.

      require

      • buffer /= Void

      append_in_unicode (buffer: UNICODE_STRING)

      Append the equivalent of to_unicode_string at the end of buffer. Thus you can save memory because no other UNICODE_STRING is allocated for the job.

      require

      • buffer /= Void

      value: NATIVE_ARRAY [E_][INTEGER]

      ensure

        value_length: INTEGER

        ensure

          put_into_mutable_big_integer (mut: MUTABLE_BIG_INTEGER)

          require

          • mut /= Void

          ensure

          • mut.to_integer_general_number.is_equal(Current)

          abs: INTEGER_GENERAL_NUMBER

          ensure

          • not Result.is_negative

          factorial: NUMBER

          require

          • is_integer_general_number
          • not is_negative

          ensure

          • Result.is_integer_general_number
          • Result.is_positive

          numerator: INTEGER_GENERAL_NUMBER
          denominator: INTEGER_GENERAL_NUMBER
          append_decimal_in (buffer: STRING, digits: INTEGER, all_digits: BOOLEAN)

          Append the equivalent of to_decimal at the end of buffer. Thus you can save memory because no other STRING is allocated.

          require

          • non_negative_digits: digits >= 0

          gcd_with_big_integer_number (other: BIG_INTEGER_NUMBER): INTEGER_GENERAL_NUMBER

          require

          • other /= Void

          integer_general_number_zero: INTEGER_GENERAL_NUMBER

          ensure

          • Result.is_zero

          integer_general_number_one: INTEGER_GENERAL_NUMBER

          ensure

          • Result.is_one

          integer_general_number_one_negative: INTEGER_GENERAL_NUMBER

          ensure

          • (-Result).is_one

          - (other: NUMBER): NUMBER

          Difference of Current and other.

          require

          • other /= Void

          ensure

          • (Result + other).is_equal(Current)

          / (other: NUMBER): NUMBER

          Quotient of Current and other.

          require

          • other /= Void
          • divisible(other)

          ensure

          • Result /= Void

          ^ (exp: NUMBER): NUMBER

          Current raised to exp-th power.

          require

          • exp.is_integer_general_number
          • is_zero implies exp @> 0

          ensure

          • Result /= Void
          • exp.is_zero implies Result.is_one

          <= (other: NUMBER): BOOLEAN

          Is Current less or equal than other?

          require

          • other_exists: other /= Void

          ensure

          • definition: Result = (Current < other or is_equal(other))

          > (other: NUMBER): BOOLEAN

          Is Current strictly greater than other?

          require

          • other_exists: other /= Void

          ensure

          • definition: Result = (other < Current)

          >= (other: NUMBER): BOOLEAN

          Is Current greater or equal than other?

          require

          • other_exists: other /= Void

          ensure

          • definition: Result = (other <= Current)

          frozen +: NUMBER

          Unary plus of Current.

          ensure

          • Result = Current

          frozen is_integer_8: BOOLEAN

          Does Current value fit on an INTEGER_8?

          ensure

          • Result implies is_integer_general_number

          frozen is_integer_16: BOOLEAN

          Does Current value fit on an INTEGER_16?

          ensure

          • Result implies is_integer_general_number

          frozen is_integer: BOOLEAN

          Does Current value fit on an INTEGER?

          ensure

          • Result implies is_integer_general_number

          is_integer_32: BOOLEAN

          Does Current value fit on an INTEGER?

          ensure

          • Result implies is_integer_general_number

          frozen is_integer_64: BOOLEAN

          Does Current value fit on an INTEGER_64?

          ensure

          • Result implies is_integer_general_number

          in_range (lower: NUMBER, upper: NUMBER): BOOLEAN

          Return True if Current is in range [lower..upper]

          ensure

          • Result = (Current >= lower and Current <= upper)

          compare (other: NUMBER): INTEGER

          Compare Current with other. < <==> Result < 0 > <==> Result > 0 Otherwise Result = 0.

          require

          • other_exists: other /= Void

          ensure

          • equal_zero: Result = 0 = is_equal(other)
          • smaller_negative: Result = -1 = (Current < other)
          • greater_positive: Result = 1 = (Current > other)

          three_way_comparison (other: NUMBER): INTEGER

          Compare Current with other. < <==> Result < 0 > <==> Result > 0 Otherwise Result = 0.

          require

          • other_exists: other /= Void

          ensure

          • equal_zero: Result = 0 = is_equal(other)
          • smaller_negative: Result = -1 = (Current < other)
          • greater_positive: Result = 1 = (Current > other)

          min (other: NUMBER): NUMBER

          Minimum of Current and other.

          require

          • other /= Void

          ensure

          • Result <= Current and then Result <= other
          • compare(Result) = 0 or else other.compare(Result) = 0

          max (other: NUMBER): NUMBER

          Maximum of Current and other.

          require

          • other /= Void

          ensure

          • Result >= Current and then Result >= other
          • compare(Result) = 0 or else other.compare(Result) = 0

          is_odd: BOOLEAN

          Is odd ?

          require

          • is_integer_general_number

          is_even: BOOLEAN

          Is even ?

          require

          • is_integer_general_number

          frozen is_integer_general_number: BOOLEAN
          frozen is_fraction_general_number: BOOLEAN
          frozen fit_real: BOOLEAN
          frozen to_integer_8: INTEGER_8

          Conversion of Current in an INTEGER_8.

          require

          • is_integer_8

          frozen to_integer_16: INTEGER_16

          Conversion of Current in an INTEGER_16.

          require

          • is_integer_16

          frozen to_integer: INTEGER

          Conversion of Current in an INTEGER.

          require

          • is_integer

          to_integer_32: INTEGER

          Conversion of Current in an INTEGER.

          require

          • is_integer

          frozen to_integer_64: INTEGER_64

          Conversion of Current in an INTEGER.

          require

          • is_integer_64

          frozen to_string: STRING

          Convert the NUMBER into a new allocated STRING. Note: see also append_in to save memory.

          frozen to_unicode_string: UNICODE_STRING

          Convert the NUMBER into a new allocated UNICODE_STRING. Note: see also append_in_unicode to save memory.

          frozen to_string_format (s: INTEGER): STRING

          Same as to_string but the result is on s character and the number is right aligned. Note: see append_in_format to save memory.

          require

          • to_string.count <= s

          ensure

          • Result.count = s

          frozen to_unicode_string_format (s: INTEGER): UNICODE_STRING

          Same as to_unicode_string but the result is on s character and the number is right aligned. Note: see append_in_unicode_format to save memory.

          require

          • to_string.count <= s

          ensure

          • Result.count = s

          frozen append_in_format (str: STRING, s: INTEGER)

          Append the equivalent of to_string_format at the end of str. Thus you can save memory because no other STRING is allocate for the job.

          require

          • to_string.count <= s

          ensure

          • str.count >= old str.count + s

          frozen append_in_unicode_format (str: UNICODE_STRING, s: INTEGER)

          Append the equivalent of to_unicode_string_format at the end of str. Thus you can save memory because no other UNICODE_STRING is allocate for the job.

          require

          • to_string.count <= s

          ensure

          • str.count >= old str.count + s

          frozen to_decimal (digits: INTEGER, all_digits: BOOLEAN): STRING

          Convert Current into its decimal view. A maximum of decimal digits places will be used for the decimal part. If the all_digits flag is True insignificant digits will be included as well. (See also decimal_in to save memory.)

          require

          • non_negative_digits: digits >= 0

          ensure

          • not Result.is_empty

          frozen decimal_digit: CHARACTER

          Gives the corresponding CHARACTER for range 0..9.

          require

          • to_integer.in_range(0, 9)

          ensure

          • (once "0123456789").has(Result)
          • Current @= Result.value

          digit: CHARACTER

          Gives the corresponding CHARACTER for range 0..9.

          require

          • to_integer.in_range(0, 9)

          ensure

          • (once "0123456789").has(Result)
          • Current @= Result.value

          divisible (other: NUMBER): BOOLEAN

          Is other a valid divisor for Current ?

          require

          • other /= Void

          one: NUMBER

          The neutral element of multiplication.

          ensure

          • neutral_element:

            Result is the neutral element of multiplication.

          zero: NUMBER

          The neutral element of addition.

          ensure

          • neutral_element:

            Result is the neutral element of addition.

          frozen sign: INTEGER_8

          Sign of Current (0 or -1 or 1).

          ensure

          • Result = 1 implies is_positive
          • Result = 0 implies is_zero
          • Result = -1 implies is_negative

          sqrt: REAL

          Compute the square routine.

          require

          • fit_real

          frozen log: REAL

          require

          • fit_real

          @- (other: INTEGER_64): NUMBER

          Difference of Current and other.

          ensure

          • Result /= Void

          @^ (exp: INTEGER_64): NUMBER

          require

          • is_zero implies exp > 0

          ensure

          • Result /= Void

          out_in_tagged_out_memory

          Append terse printable represention of current object in tagged_out_memory.

          ensure

          • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
          • append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))

          fill_tagged_out_memory

          Append a viewable information in tagged_out_memory in order to affect the behavior of out, tagged_out, etc.

          frozen add_with_integer_64_number (other: INTEGER_64_NUMBER): NUMBER

          require

          • other /= Void

          ensure

          • Result /= Void

          multiply_with_integer_64_number (other: INTEGER_64_NUMBER): NUMBER

          require

          • other /= Void

          ensure

          • Result /= Void

          greater_with_integer_64_number (other: INTEGER_64_NUMBER): BOOLEAN

          require

          • other /= Void

          max_double: NUMBER
          min_double: NUMBER
          mutable_register1: MUTABLE_BIG_INTEGER
          mutable_register2: MUTABLE_BIG_INTEGER
          mutable_register3: MUTABLE_BIG_INTEGER
          mutable_register4: MUTABLE_BIG_INTEGER
          deferred is_equal (other: BIG_INTEGER_NUMBER): BOOLEAN

          Is other attached to an object considered equal to current object ?

          require

          • other /= Void

          ensure

          • Result implies hash_code = other.hash_code
          • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

          is_equal (other: BIG_INTEGER_NUMBER): BOOLEAN

          Is other attached to an object considered equal to current object ?

          require

          • other /= Void

          ensure

          • trichotomy: Result = (not (Current < other) and not (other < Current))
          • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

          Class invariant