+
Point of view
All features
class MUTABLE_BIG_INTEGER
Summary
top
A class used to represent multiprecision integers that makes efficient use of allocated space by allowing a number to occupy only part of an array so that the arrays do not have to be reallocated as often. When performing an operation with many iterations the array used to hold a number is only reallocated when necessary and does not have to be the same size as the number it represents. A mutable number allows calculations to occur on the same number without having to create a new number for every step of the calculation as it occurs with NUMBERs.
Direct parents
Inherit list: COMPARABLE, HASHABLE
Insert list: PLATFORM
Class invariant
top
Overview
top
Creation features
{ANY}
  • from_integer (value: INTEGER_32)
    Create or initialize Current using value as an initializer.
  • from_integer_64 (value: INTEGER_64)
    Create or set Current using value as an initializer.
  • from_string (str: STRING)
    Create or initialize Current using value as an initializer.
  • copy (other: MUTABLE_BIG_INTEGER)
    Update current object using fields of object attached to other, so as to yield equal objects.
Features
Creation / initialization from INTEGER_32 or INTEGER_64:
{ANY}
Creation / initialization from STRING:
{ANY}
  • from_string (str: STRING)
    Create or initialize Current using value as an initializer.
Conversion tool
{ANY}
  • force_to_real_64: REAL_64
    only a tool unsigned conversion *** require ou changer export ? *** (Dom Oct 4th 2004) ***
{NUMBER}
Addition:
{ANY}
  • add (other: MUTABLE_BIG_INTEGER)
    Add other into Current.
  • add_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
    Add other and Current, and put the result in res.
  • add_integer (other: INTEGER_32)
    Add other into Current.
  • add_integer_64 (other: INTEGER_64)
    Add other into Current.
  • add_natural (other: MUTABLE_BIG_INTEGER)
    Same behavior as add, but this one works only when Current and other are both positive numbers and are both greater than zero.
Subtract:
{ANY}
To divide:
{ANY}
  • divide (other: MUTABLE_BIG_INTEGER)
    Put the quotient of the Euclidian division of Current by other in Current.
  • mod (other: MUTABLE_BIG_INTEGER)
    Put the remainder of the Euclidian division of Current by other in Current.
  • divide_with_remainder_to (other: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)
    Euclidian division.
  • remainder_with_quotient_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER)
    Euclidian division.
  • divide_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)
    Euclidian division.
  • shift_left (n: INTEGER_32)
    Shift bits of magnitude by n position left.
  • shift_right (n: INTEGER_32)
    Right shift Current n bits.
GCD
{ANY}
  • gcd (other: MUTABLE_BIG_INTEGER)
    Compute GCD of Current and other.
To multiply:
{ANY}
  • multiply (other: MUTABLE_BIG_INTEGER)
    Multiply Current by other.
  • multiply_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
    Multiply the contents of Current and other and place the result in res.
  • multiply_integer (other: INTEGER_32, res: MUTABLE_BIG_INTEGER)
    Multiply the contents of Current and other and place the result in res.
to multiply
{MUTABLE_BIG_INTEGER}
Comparison:
{ANY}
Printing:
{ANY}
Miscellaneous:
{ANY}
  • negate
    Negate the sign of Current.
  • abs
    Absolute value of Current.
  • sign: INTEGER_8
    Sign of Current (0 -1 or 1).
  • set_with_zero
  • hash_code: INTEGER_32
    The hash-code value of Current.
  • copy (other: MUTABLE_BIG_INTEGER)
    Update current object using fields of object attached to other, so as to yield equal objects.
  • swap_with (other: MUTABLE_BIG_INTEGER)
    Swap the value of Current with the value of other.
{MUTABLE_BIG_INTEGER}
Implementation:
{MUTABLE_BIG_INTEGER}
Implementation:
{MUTABLE_BIG_INTEGER}
For printing
{}
Tools for capacity:
{}
{}
{ANY}
  • infix "<=" (other: MUTABLE_BIG_INTEGER): BOOLEAN
    Is Current less than or equal other?
  • infix ">" (other: MUTABLE_BIG_INTEGER): BOOLEAN
    Is Current strictly greater than other?
  • infix ">=" (other: MUTABLE_BIG_INTEGER): BOOLEAN
    Is Current greater than or equal than other?
  • in_range (lower: MUTABLE_BIG_INTEGER, upper: MUTABLE_BIG_INTEGER): BOOLEAN
    Return True if Current is in range [lower..upper]
    See also min, max, compare.
  • compare (other: MUTABLE_BIG_INTEGER): INTEGER_32
    If current object equal to other, 0 if smaller, -1; if greater, 1.
  • three_way_comparison (other: MUTABLE_BIG_INTEGER): INTEGER_32
    If current object equal to other, 0 if smaller, -1; if greater, 1.
  • min (other: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
    Minimum of Current and other.
  • max (other: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
    Maximum of Current and other.
  • bounded_by (a_min: MUTABLE_BIG_INTEGER, a_max: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
    A value that is equal to Current if it is between the limits set by a_min and a_max.
Maximum:
{}
Minimum:
{}
Bits:
{}
from_integer (value: INTEGER_32)
effective procedure
{ANY}
top
Create or initialize Current using value as an initializer.
ensure
is_integer_32: BOOLEAN
effective function
{ANY}
top
Does Current fit on an INTEGER_32?
ensure
to_integer_32: INTEGER_32
effective function
{ANY}
top
Convert Current as a 32 bit INTEGER.
require
from_integer_64 (value: INTEGER_64)
effective procedure
{ANY}
top
Create or set Current using value as an initializer.
ensure
is_integer_64: BOOLEAN
effective function
{ANY}
top
Does Current fit on an INTEGER_64?
ensure
to_integer_64: INTEGER_64
effective function
{ANY}
top
Convert Current as a INTEGER_64.
require
from_string (str: STRING)
effective procedure
{ANY}
top
Create or initialize Current using value as an initializer.
(value = [-][0-9]^+)
force_to_real_64: REAL_64
effective function
{ANY}
top
only a tool unsigned conversion *** require ou changer export ? *** (Dom Oct 4th 2004) ***
from_native_array (na: NATIVE_ARRAY[INTEGER_32], cap: INTEGER_32, neg: BOOLEAN)
effective procedure
{NUMBER}
top
require
  • na.item(cap - 1) /= 0
to_integer_general_number: INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
add (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Add other into Current.
See also add_integer, add_integer_64, add_natural.
require
  • other /= Void
add_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Add other and Current, and put the result in res.
require
  • other /= Void
  • res /= Void
  • res /= Current
  • res /= other
add_integer (other: INTEGER_32)
effective procedure
{ANY}
top
Add other into Current.
add_integer_64 (other: INTEGER_64)
effective procedure
{ANY}
top
Add other into Current.
add_natural (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Same behavior as add, but this one works only when Current and other are both positive numbers and are both greater than zero.
The only one advantage of using add_natural instead of the general add is the gain of efficiency.
require
subtract (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Subtract other from Current.
require
  • other /= Void
subtract_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Subtract other from Current and put it in res.
require
  • other /= Void
  • res /= Void
  • res /= Current
  • res /= other
subtract_integer (other: INTEGER_32)
effective procedure
{ANY}
top
divide (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Put the quotient of the Euclidian division of Current by other in Current.
(The contents of other is not changed.)
require
  • not other.is_zero
  • other /= Current
mod (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Put the remainder of the Euclidian division of Current by other in Current.
(The contents of other is not changed.)
require
  • not other.is_zero
  • other /= Current
ensure
divide_with_remainder_to (other: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Euclidian division.
Calculates the quotient and remainder of Current divided by other. Quotient is put in Current. (The contents of other is not changed.)
require
  • not other.is_zero
  • remainder /= Void
  • remainder /= other
  • remainder /= Current
ensure
remainder_with_quotient_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Euclidian division.
Calculates the quotient and remainder of Current divided by other. Remainder is put in Current. (The contents of other is not changed.)
Note: Uses Algorithm D in Knuth section 4.3.1.
require
  • not other.is_zero
  • quotient /= Void
  • quotient /= other
  • quotient /= Current
ensure
divide_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Euclidian division.
Calculates the quotient and remainder of Current divided by other. (The contents of Current and other are not changed.)
Note: Uses Algorithm D in Knuth section 4.3.1.
require
  • not other.is_zero
  • quotient /= Void
  • remainder /= Void
  • quotient /= other
  • quotient /= Current
  • remainder /= other
  • remainder /= Current
ensure
shift_left (n: INTEGER_32)
effective procedure
{ANY}
top
Shift bits of magnitude by n position left.
(Note that no bit can be lost because the storage area is automatically extended when it is necessary.)
require
  • n > 0
shift_right (n: INTEGER_32)
effective procedure
{ANY}
top
Right shift Current n bits.
(Current is left in normal form.)
require
  • n > 0
gcd (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Compute GCD of Current and other.
GCD is put in Current (other is not modified).
require
  • other /= Void
ensure
multiply (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Multiply Current by other.
require
  • other /= Void
multiply_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Multiply the contents of Current and other and place the result in res.
(Current and other are not modified.)
require
  • other /= Void
  • res /= Void
  • res /= Current
multiply_integer (other: INTEGER_32, res: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Multiply the contents of Current and other and place the result in res.
(Current is not modified.)
require
  • res /= Current
  • res /= Void
multiply_like_human (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Simple multiply.
Complexity = O(integer_length*other.integer_length).
require
multiply_like_human_aux (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Only used by multiply_to_like_human.
require
multiply_like_human_aux_reverse (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Only used by multiply_to_like_human.
require
multiply_to_like_human (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Simple multiply.
Complexity = O(integer_length*other.integer_length).
require
is_zero: BOOLEAN
effective function
{ANY}
top
Is it 0?
ensure
is_one: BOOLEAN
effective function
{ANY}
top
Is it 1?
ensure
is_one_negative: BOOLEAN
effective function
{ANY}
top
Is it -1 ?
ensure
is_negative: BOOLEAN
effective function
{ANY}
top
Is Current negative integer?
ensure
is_positive: BOOLEAN
effective function
{ANY}
top
Is Current positive integer?
ensure
is_even: BOOLEAN
effective function
{ANY}
top
Is Current even?
ensure
is_odd: BOOLEAN
effective function
{ANY}
top
Is Current odd?
ensure
is_equal (other: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Is other attached to an object considered equal to current object?
require
    • other /= Void
    • other /= Void
ensure
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
  • Result implies hash_code = other.hash_code
  • trichotomy: Result = not Current < other and not other < Current
infix "<" (other: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Is Current strictly less than other?
See also >, <=, >=, min, max.
require
  • other_exists: other /= Void
ensure
  • asymmetric: Result implies not other < Current
abs_compare (other: MUTABLE_BIG_INTEGER): INTEGER_32
effective function
{ANY}
top
Compare the magnitude of Current and other.
Returns -1, 0 or 1 as this MutableBigInteger is numerically less than, equal to, or greater than other.
to_string: STRING
effective function
{ANY}
top
The decimal view of Current into a new allocated STRING.
For example, if Current is -1 the Result is "-1".
See also append_in, to_string_format, to_unicode_string, to_integer.
to_unicode_string: UNICODE_STRING
effective function
{ANY}
top
The decimal view of Current into a new allocated UNICODE_STRING.
For example, if Current represents -1 the Result is U"-1".
See also append_in_unicode, to_unicode_string_format, to_string.
append_in (buffer: STRING)
effective procedure
{ANY}
top
Append in the buffer the equivalent of to_string.
No new STRING creation during the process.
require
append_in_unicode (buffer: UNICODE_STRING)
effective procedure
{ANY}
top
Append in the buffer the equivalent of to_string.
No new STRING creation during the process.
require
to_string_format (s: INTEGER_32): STRING
effective function
{ANY}
top
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 ensure
  • Result.count = s
to_unicode_string_format (s: INTEGER_32): UNICODE_STRING
effective function
{ANY}
top
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 ensure
  • Result.count = s
append_in_format (str: STRING, s: INTEGER_32)
effective procedure
{ANY}
top
Append the equivalent of to_string_format at the end of str.
Thus you can save memory because no other STRING is allocated for the job.
require ensure
  • str.count >= old str.count + s
append_in_unicode_format (str: UNICODE_STRING, s: INTEGER_32)
effective procedure
{ANY}
top
Append the equivalent of to_unicode_string_format at the end of str.
Thus you can save memory because no other UNICODE_STRING is allocated for the job.
require ensure
  • str.count >= old str.count + s
is_printable: BOOLEAN
effective function
{ANY}
top
True if decimal view of Current is short enough to be put in a STRING.
out_in_tagged_out_memory
effective procedure
{ANY}
top
Append terse printable representation of current object in tagged_out_memory.
require
    • locked: tagged_out_locked
    • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • 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
effective procedure
{ANY}
top
Append a viewable information in tagged_out_memory in order to affect the behavior of out, tagged_out, etc.
require
    • locked: tagged_out_locked
    • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
negate
effective procedure
{ANY}
top
Negate the sign of Current.
abs
effective procedure
{ANY}
top
Absolute value of Current.
sign: INTEGER_8
effective function
{ANY}
top
Sign of Current (0 -1 or 1).
set_with_zero
effective procedure
{ANY}
top
ensure
hash_code: INTEGER_32
effective function
{ANY}
top
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
copy (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Update current object using fields of object attached to other, so as to yield equal objects.
Note: you can't copy object from a different dynamic type.
require
    • not immutable
    • same_dynamic_type(other)
    • not immutable
    • same_dynamic_type(other)
ensure
  • is_equal(other)
swap_with (other: MUTABLE_BIG_INTEGER)
effective procedure
{ANY}
top
Swap the value of Current with the value of other.
writable attribute
{MUTABLE_BIG_INTEGER}
top
Holds the magnitude of Current in natural order (the most significant INTEGER_32 word has the highest address).
To avoid many reallocation of this storage area, only some words are significant. The magnitude is stored in the following significant range [offset .. offset + integer_length - 1].
capacity: INTEGER_32
writable attribute
{MUTABLE_BIG_INTEGER}
top
Of the allocated storage area.
integer_length: INTEGER_32
writable attribute
{MUTABLE_BIG_INTEGER}
top
The number of significant INTEGER_32 words in the storage area.
offset: INTEGER_32
writable attribute
{MUTABLE_BIG_INTEGER}
top
The offset of the less significant word into the storage area.
negative: BOOLEAN
writable attribute
{MUTABLE_BIG_INTEGER}
top
True when Current is negative.
item (index: INTEGER_32): INTEGER_32
effective function
{MUTABLE_BIG_INTEGER}
top
require
put (value: INTEGER_32, index: INTEGER_32)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require
set_negative (n: BOOLEAN)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require ensure
set_integer_length (il: INTEGER_32)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require ensure
set_offset (o: INTEGER_32)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require ensure
set_ilo (il: INTEGER_32, o: INTEGER_32)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require ensure
set_storage (new_storage: NATIVE_ARRAY[INTEGER_32])
effective procedure
{MUTABLE_BIG_INTEGER}
top
set_capacity (new_capacity: INTEGER_32)
effective procedure
{MUTABLE_BIG_INTEGER}
top
set_all (new_storage: NATIVE_ARRAY[INTEGER_32], new_capacity: INTEGER_32, new_integer_length: INTEGER_32, new_offset: INTEGER_32, new_negative: BOOLEAN)
effective procedure
{MUTABLE_BIG_INTEGER}
top
require
  • new_capacity > 0
  • new_storage.is_not_null
  • new_integer_length.in_range(0, new_capacity)
  • new_integer_length /= 0 implies new_offset.in_range(0, new_capacity - new_integer_length) and new_storage.item(new_offset + new_integer_length - 1) /= 0
  • new_integer_length = 0 implies not new_negative
  • new_capacity.is_a_power_of_2
ensure
primitive_shift_left (n: INTEGER_8)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Left shift Current with no need to extend the storage.
|*** Can be a little faster (Vincent Croizier, 26/04/04) ***
require
primitive_shift_right (n: INTEGER_8)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Right shift Current of n bits.
require ensure
divide_one_word (divisor: INTEGER_32): INTEGER_32
effective function
{MUTABLE_BIG_INTEGER}
top
This method is used by divide.
The one word divisor specified by divisor is saw as unsigned. Current is the dividend (saw positive) at invocation but is replaced by the quotient. The remainder is returned as unsigned INTEGER. Note: Current is modified by this method.
require
  • divisor /= 0
divide_sign_correction (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Correct the value of quotient and remainder after an "unsigned" division.
Only used by divide.
require ensure
divide_sign_correction_bis (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, current_negative: BOOLEAN)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Correct the value of quotient and remainder after an "unsigned" division.
Only used by divide.
require ensure
multiply_and_subtract (u1: INTEGER_32, qhat: INTEGER_32, d_storage: NATIVE_ARRAY[INTEGER_32], d_offset: INTEGER_32, r_storage: NATIVE_ARRAY[INTEGER_32], r_offset: INTEGER_32, length: INTEGER_32): BOOLEAN
effective function
{MUTABLE_BIG_INTEGER}
top
Only used by divide.
require
  • qhat /= 0
add_back (old_u1: INTEGER_32, d_storage: NATIVE_ARRAY[INTEGER_32], d_offset: INTEGER_32, r_storage: NATIVE_ARRAY[INTEGER_32], r_offset: INTEGER_32, length: INTEGER_32): BOOLEAN
effective function
{MUTABLE_BIG_INTEGER}
top
Only used by divide.
old_u1 is the value of u1 before multiply_and_subtract.
is_a_good_divide (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{MUTABLE_BIG_INTEGER}
top
require
  • other /= Void
  • quotient /= Void
  • remainder /= Void
normalize: INTEGER_8
effective function
{MUTABLE_BIG_INTEGER}
top
Shift left until the most significant bit is on.
Result give the number of left shift.
require ensure
register1: MUTABLE_BIG_INTEGER
once function
{MUTABLE_BIG_INTEGER}
top
register2: MUTABLE_BIG_INTEGER
once function
{MUTABLE_BIG_INTEGER}
top
Real_base: REAL_64
once function
{MUTABLE_BIG_INTEGER}
top
add_magnitude (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Add the magnitude of Current and other regardless of signs.
require
subtract_magnitude (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Subtract other from Current (The result is placed in Current) and change negative (the sign) if necessary.
require
subtract_magnitude_raw (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Subtract (raw) the storage of other from Current.
Used by subtract_magnitude.
require ensure
subtract_magnitude_raw_reverse (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Subtract (raw) the storage of Current from other and put it in Current.
Used by subtract_magnitude.
require ensure
subtract_magnitude_raw_truncated (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Subtract (raw) the storage of other from Current where other is truncated to the size of Current.
subtract_magnitude_raw_reverse_truncated (other: MUTABLE_BIG_INTEGER)
effective procedure
{MUTABLE_BIG_INTEGER}
top
Subtract (raw) the storage of Current from other and put it in Current, where other is truncated to the size of Current.
char_buffer: FAST_ARRAY[CHARACTER]
once function
{}
top
append_in_char_buffer: INTEGER_32
effective function
{}
top
Tool for append_in and append_in_unicode.
Put absolute value of Current in char_buffer and return the number of characteres really used.
require
capacity_from_lower_bound (actual_capacity: INTEGER_32, needed_capacity: INTEGER_32): INTEGER_32
effective function
{}
top
Give the smallest power of 2 greater than needed_capacity and actual_capacity.
Based on actual_capacity (the actual capacity).
require
  • actual_capacity.is_a_power_of_2
  • actual_capacity >= 4
ensure
  • Result.is_a_power_of_2
  • Result >= 4
  • Result >= actual_capacity
  • Result >= needed_capacity
  • Result = actual_capacity or Result #// 2 < needed_capacity
capacity_from_upper_bound (actual_capacity: INTEGER_32, needed_capacity: INTEGER_32): INTEGER_32
effective function
{}
top
Give the smallest power of 2 greater than needed_capacity.
Based on actual_capacity (the actual capacity).
require
  • actual_capacity >= 4
  • actual_capacity >= needed_capacity
  • actual_capacity.is_a_power_of_2
ensure
  • Result.is_a_power_of_2
  • Result <= actual_capacity
  • Result >= needed_capacity
  • Result = 4 or Result.bit_shift_right(1) < needed_capacity
unsigned_less_than (a: INTEGER_32, b: INTEGER_32): BOOLEAN
{}
top
Unsigned "<".
unsigned_greater_than (a: INTEGER_32, b: INTEGER_32): BOOLEAN
{}
top
Unsigned ">".
unsigned_greater_or_equal (a: INTEGER_32, b: INTEGER_32): BOOLEAN
{}
top
Unsigned ">=".
unsigned_32_to_integer_64 (integer_32: INTEGER_32): INTEGER_64
{}
top
Return the unsigned value of the integer_32.
storage_at (s: NATIVE_ARRAY[INTEGER_32], n: INTEGER_32): POINTER
{}
top
Give the address of the corresponding word of s.
mbi_inc (integer_32_adr: POINTER): BOOLEAN
{}
top
Increment the value at integer_32_adr.
The Result is True only in case of overflow.
mbi_add (a: INTEGER_32, b: INTEGER_32, integer_32_adr: POINTER): BOOLEAN
{}
top
t.item(n) := a + b Overflow if "Result = True".
mbi_add_with_inc (a: INTEGER_32, b: INTEGER_32, integer_32_adr: POINTER): BOOLEAN
{}
top
t.item(n) := a + b + 1 Overflow if "Result = True".
mbi_dec (integer_32_adr: POINTER): BOOLEAN
{}
top
Put a - 1 in the item n in the NATIVE_ARRAY t.
t.item(n) := a - 1 Underflow if "Result = True".
mbi_subtract (a: INTEGER_32, b: INTEGER_32, integer_32_adr: POINTER): BOOLEAN
{}
top
t.item(n) := a - b Underflow if "Result = True".
mbi_subtract_with_dec (a: INTEGER_32, b: INTEGER_32, integer_32_adr: POINTER): BOOLEAN
{}
top
t.item(n) := a - b - 1 Underflow if "Result = True".
mbi_multiply (a: INTEGER_32, b: INTEGER_32, integer_32_adr: POINTER): INTEGER_32
{}
top
put a * b in t@n and return the overflow.
mbi_multiply_with_add (a: INTEGER_32, b: INTEGER_32, c: INTEGER_32, integer_32_adr: POINTER): INTEGER_32
{}
top
put a * b + c in t@n and return the overflow.
mbi_multiply_with_2_add (a: INTEGER_32, b: INTEGER_32, c: INTEGER_32, d: INTEGER_32, integer_32_adr: POINTER): INTEGER_32
{}
top
put a * b + c + d in t@n and return the overflow.
mbi_divide (u1: INTEGER_32, u0: INTEGER_32, d: INTEGER_32, r_int32adr: POINTER): INTEGER_32
{}
top
Divide u1u0 by d, put the remainder in r and return the quotient.
string_buffer: STRING
once function
{}
top
unicode_string_buffer: UNICODE_STRING
once function
{}
top
infix "<=" (other: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Is Current less than or equal other?
See also >=, <, >, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = Current < other or is_equal(other)
infix ">" (other: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Is Current strictly greater than other?
See also <, >=, <=, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = other < Current
infix ">=" (other: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Is Current greater than or equal than other?
See also <=, >, <, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = other <= Current
in_range (lower: MUTABLE_BIG_INTEGER, upper: MUTABLE_BIG_INTEGER): BOOLEAN
effective function
{ANY}
top
Return True if Current is in range [lower..upper]
See also min, max, compare.
ensure
  • Result = Current >= lower and Current <= upper
compare (other: MUTABLE_BIG_INTEGER): INTEGER_32
effective function
{ANY}
top
If current object equal to other, 0 if smaller, -1; if greater, 1.
See also min, max, in_range.
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: MUTABLE_BIG_INTEGER): INTEGER_32
effective function
{ANY}
top
If current object equal to other, 0 if smaller, -1; if greater, 1.
See also min, max, in_range.
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: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
effective function
{ANY}
top
Minimum of Current and other.
See also max, in_range.
require
  • other /= Void
ensure
  • Result <= Current and then Result <= other
  • compare(Result) = 0 or else other.compare(Result) = 0
max (other: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
effective function
{ANY}
top
Maximum of Current and other.
See also min, in_range.
require
  • other /= Void
ensure
  • Result >= Current and then Result >= other
  • compare(Result) = 0 or else other.compare(Result) = 0
bounded_by (a_min: MUTABLE_BIG_INTEGER, a_max: MUTABLE_BIG_INTEGER): MUTABLE_BIG_INTEGER
effective function
{ANY}
top
A value that is equal to Current if it is between the limits set by a_min and a_max.
Otherwise it's a_min if Current is smaller or a_max if Current is greater It's a shortcut for Current.min(a_max).max(a_min) also known as "clamp" in the widespread C library Glib
ensure
  • correctness: Result.in_range(a_min, a_max)
Maximum_character_code: INTEGER_16
{}
top
Largest supported code for CHARACTER values.
ensure
  • meaningful: Result >= 127
Maximum_integer_8: INTEGER_8
is 127
constant attribute
{}
top
Largest supported value of type INTEGER_8.
Maximum_integer_16: INTEGER_16
is 32767
constant attribute
{}
top
Largest supported value of type INTEGER_16.
Maximum_integer: INTEGER_32
is 2147483647
constant attribute
{}
top
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_32: INTEGER_32
is 2147483647
constant attribute
{}
top
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_64: INTEGER_64
is 9223372036854775807
constant attribute
{}
top
Largest supported value of type INTEGER_64.
Maximum_real_32: REAL_32
is {REAL_32 3.4028234663852885981170418348451692544e+38}
constant attribute
{}
top
Largest non-special (no NaNs nor infinity) supported value of type REAL_32.
Maximum_real: REAL_64
{}
top
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_64
{}
top
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
{}
top
Largest supported value of type REAL_80.
ensure
Minimum_character_code: INTEGER_16
{}
top
Smallest supported code for CHARACTER values.
ensure
  • meaningful: Result <= 0
Minimum_integer_8: INTEGER_8
is -128
constant attribute
{}
top
Smallest supported value of type INTEGER_8.
Minimum_integer_16: INTEGER_16
is -32768
constant attribute
{}
top
Smallest supported value of type INTEGER_16.
Minimum_integer: INTEGER_32
is -2147483648
constant attribute
{}
top
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_32: INTEGER_32
is -2147483648
constant attribute
{}
top
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_64: INTEGER_64
is -9223372036854775808
constant attribute
{}
top
Smallest supported value of type INTEGER_64.
Minimum_real_32: REAL_32
is {REAL_32 -3.40282346638528859811704183484516925440e+38}
constant attribute
{}
top
Smallest non-special (no NaNs nor infinity) supported value of type REAL_32.
Minimum_real: REAL_64
{}
top
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_64
{}
top
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_64
{}
top
Smallest supported value of type REAL_80.
ensure
  • meaningful: Result <= 0.0
Boolean_bits: INTEGER_32
{}
top
Number of bits in a value of type BOOLEAN.
ensure
  • meaningful: Result >= 1
Character_bits: INTEGER_32
{}
top
Number of bits in a value of type CHARACTER.
ensure
Integer_bits: INTEGER_32
{}
top
Number of bits in a value of type INTEGER.
ensure
  • integer_definition: Result = 32
Real_bits: INTEGER_32
is 64
constant attribute
{}
top
Number of bits in a value of type REAL.
Pointer_bits: INTEGER_32
{}
top
Number of bits in a value of type POINTER.