class BIG_INTEGER_NUMBER

All features

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

To create fractions

Maximum:

Minimum:

Bits:

Details

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

require

    ensure

    • capacity = cap
    • storage = na
    • negative = neg

    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

    • Result = storage

    value_length: INTEGER

    ensure

    • Result = capacity

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

    require

      ensure

      • capacity = cap
      • storage = na
      • negative = neg

      put_into_mutable_big_integer (mut: MUTABLE_BIG_INTEGER)

      require

      • mut /= Void

      ensure

      • mut.to_integer_general_number.is_equal(Current)

      negative: BOOLEAN
      capacity: INTEGER
      storage: NATIVE_ARRAY [E_][INTEGER]
      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
      string_buffer: STRING
      unicode_string_buffer: UNICODE_STRING
      from_two_integer (n: INTEGER_64, d: INTEGER_64): NUMBER

      require

      • d /= 0

      ensure

      • Result @* d @= n

      from_two_integer_general_number (n: INTEGER_GENERAL_NUMBER, d: INTEGER_GENERAL_NUMBER): NUMBER

      require

      • n /= Void
      • d /= Void
      • not d.is_zero

      ensure

      • n.is_equal(Result * d)

      from_integer_and_integer_general_number (n: INTEGER_64, d: INTEGER_GENERAL_NUMBER): NUMBER

      require

      • d /= Void
      • not d.is_zero

      from_integer_general_number_and_integer (n: INTEGER_GENERAL_NUMBER, d: INTEGER_64): NUMBER

      require

      • n /= Void
      • d /= 0

      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)

      Maximum_character_code: INTEGER_16

      Largest supported code for CHARACTER values.

      ensure

      • meaningful: Result >= 127

      Maximum_integer_8: INTEGER_8

      Largest supported value of type INTEGER_8.

      Maximum_integer_16: INTEGER_16

      Largest supported value of type INTEGER_16.

      Maximum_integer: INTEGER

      Largest supported value of type INTEGER/INTEGER_32.

      Maximum_integer_32: INTEGER

      Largest supported value of type INTEGER/INTEGER_32.

      Maximum_integer_64: INTEGER_64

      Largest supported value of type INTEGER_64.

      Maximum_real_32: REAL_32

      Largest non-special (no NaNs nor infinity) supported value of type REAL_32.

      Maximum_real: REAL

      Largest non-special (no NaNs nor infinity) supported value of type REAL. Just to give an idea of this value: 1.79769313486231570....e+308

      Maximum_real_64: REAL

      Largest non-special (no NaNs nor infinity) supported value of type REAL. Just to give an idea of this value: 1.79769313486231570....e+308

      Maximum_real_80: REAL_EXTENDED

      Largest supported value of type REAL_80.

      ensure

      • meaningful: Result >= Maximum_real

      Minimum_character_code: INTEGER_16

      Smallest supported code for CHARACTER values.

      ensure

      • meaningful: Result <= 0

      Minimum_integer_8: INTEGER_8

      Smallest supported value of type INTEGER_8.

      Minimum_integer_16: INTEGER_16

      Smallest supported value of type INTEGER_16.

      Minimum_integer: INTEGER

      Smallest supported value of type INTEGER/INTEGER_32.

      Minimum_integer_32: INTEGER

      Smallest supported value of type INTEGER/INTEGER_32.

      Minimum_integer_64: INTEGER_64

      Smallest supported value of type INTEGER_64.

      Minimum_real_32: REAL_32

      Smallest non-special (no NaNs nor infinity) supported value of type REAL_32.

      Minimum_real: REAL

      Smallest non-special (no NaNs nor infinity) supported value of type REAL. Just to give an idea of this value: -1.79769313486231570....e+308

      Minimum_real_64: REAL

      Smallest non-special (no NaNs nor infinity) supported value of type REAL. Just to give an idea of this value: -1.79769313486231570....e+308

      Minimum_real_80: REAL

      Smallest supported value of type REAL_80.

      ensure

      • meaningful: Result <= 0.0

      Boolean_bits: INTEGER

      Number of bits in a value of type BOOLEAN.

      ensure

      • meaningful: Result >= 1

      Character_bits: INTEGER

      Number of bits in a value of type CHARACTER.

      ensure

      • meaningful: Result >= 1
      • large_enough: 2.to_integer ^ Result >= Maximum_character_code

      Integer_bits: INTEGER

      Number of bits in a value of type INTEGER.

      ensure

      • integer_definition: Result = 32

      Real_bits: INTEGER

      Number of bits in a value of type REAL.

      Pointer_bits: INTEGER

      Number of bits in a value of type POINTER.

      Class invariant