class BIG_INTEGER_NUMBER

Features exported to INTERNALS_HANDLER

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

Direct parents

conformant parents

INTEGER_GENERAL_NUMBER

Summary

creation features

exported features

Misc:

comparisons with NUMBER

comparisons with REAL_64

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:

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

      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)

      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

      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

      - (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.

      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