class MUTABLE_BIG_INTEGER

All features

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

conformant parents

COMPARABLE, HASHABLE

non-conformant parents

PLATFORM

Summary

creation features

exported features

Creation / initialization from INTEGER_32 or INTEGER_64:

Creation / initialization from STRING:

Conversion tool

Addition:

Subtract:

To divide:

GCD

To multiply:

to multiply

Comparison:

Printing:

Miscellaneous:

Implementation:

Implementation:

For printing

Tools for capacity:

Maximum:

Minimum:

Bits:

Details

from_integer (value: INTEGER)

Create or initialize Current using value as an initializer.

ensure

  • to_integer = value

from_integer_64 (value: INTEGER_64)

Create or set Current using value as an initializer.

ensure

  • to_integer_64 = value

from_string (str: STRING)

Create or initialize Current using value as an initializer. (value = [-][0-9]^+)

copy (other: MUTABLE_BIG_INTEGER)

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

  • same_dynamic_type(other)

ensure

  • is_equal(other)

from_integer (value: INTEGER)

Create or initialize Current using value as an initializer.

ensure

  • to_integer = value

is_integer: BOOLEAN

Does Current fit on an INTEGER_32?

ensure

  • Result implies is_integer_64
  • Result implies integer_length <= 1

to_integer: INTEGER

Convert Current as a 32 bit INTEGER.

require

  • is_integer

from_integer_64 (value: INTEGER_64)

Create or set Current using value as an initializer.

ensure

  • to_integer_64 = value

is_integer_64: BOOLEAN

Does Current fit on an INTEGER_64?

ensure

  • not Result implies not is_integer
  • Result implies integer_length <= 2

to_integer_64: INTEGER_64

Convert Current as a INTEGER_64.

require

  • is_integer_64

from_string (str: STRING)

Create or initialize Current using value as an initializer. (value = [-][0-9]^+)

force_to_real_64: REAL

only a tool unsigned conversion *** require ou changer export ? *** (Dom Oct 4th 2004) ***

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

require

  • na.item(cap - 1) /= 0

to_integer_general_number: INTEGER_GENERAL_NUMBER
add (other: MUTABLE_BIG_INTEGER)

Add other into Current. (See also add_integer add_integer_64 and add_natural.)

require

  • other /= Void

add_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)

Add other and Current, and put the result in res.

require

  • other /= Void
  • res /= Void
  • res /= Current
  • res /= other

add_integer (other: INTEGER)

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. The only one advantage of using add_natural instead of the general add is the gain of efficiency.

require

  • not is_zero and not is_negative
  • not other.is_zero and not other.is_negative

subtract (other: MUTABLE_BIG_INTEGER)

Subtract other from Current.

require

  • other /= Void

subtract_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)

Subtract other from Current and put it in res.

require

  • other /= Void
  • res /= Void
  • res /= Current
  • res /= other

subtract_integer (other: INTEGER)
divide (other: MUTABLE_BIG_INTEGER)

Put the 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)

Put the 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

  • not negative and abs_compare(other) = -1

divide_with_remainder_to (other: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)

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

  • not remainder.negative and remainder.abs_compare(other) = -1

remainder_with_quotient_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER)

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

  • not negative and abs_compare(other) = -1

divide_to (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, remainder: MUTABLE_BIG_INTEGER)

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

  • is_a_good_divide(other, quotient, remainder)
  • not remainder.negative and remainder.abs_compare(other) = -1

shift_left (n: INTEGER)

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)

Right shift Current n bits. (Current is left in normal form.)

require

  • n > 0

gcd (other: MUTABLE_BIG_INTEGER)

Compute GCD of Current and other. GCD is put in Current (other is not modified).

require

  • other /= Void

ensure

  • is_positive or is_zero and other.is_zero

multiply (other: MUTABLE_BIG_INTEGER)

Multiply Current by other.

require

  • other /= Void

multiply_to (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)

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, res: MUTABLE_BIG_INTEGER)

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)

Simple multiply. Complexity = O(integer_length*other.integer_length).

require

  • not is_zero
  • not other.is_zero

multiply_like_human_aux (other: MUTABLE_BIG_INTEGER)

Only used by multiply_to_like_human.

require

  • not is_zero
  • not other.is_zero
  • offset >= other.integer_length

multiply_like_human_aux_reverse (other: MUTABLE_BIG_INTEGER)

Only used by multiply_to_like_human.

require

  • not is_zero
  • not other.is_zero
  • offset + integer_length <= capacity - other.integer_length

multiply_to_like_human (other: MUTABLE_BIG_INTEGER, res: MUTABLE_BIG_INTEGER)

Simple multiply. Complexity = O(integer_length*other.integer_length).

require

  • res /= Current
  • not is_zero
  • not other.is_zero

is_zero: BOOLEAN

Is it 0?

ensure

  • Result implies not is_negative

is_one: BOOLEAN

Is it 1?

ensure

  • Result implies not is_negative

is_one_negative: BOOLEAN

Is it -1 ?

ensure

  • Result implies is_negative

is_negative: BOOLEAN

Is Current negative integer?

ensure

  • Result implies not is_positive

is_positive: BOOLEAN

Is Current positive integer?

ensure

  • Result implies not is_negative

is_even: BOOLEAN

Is Current even?

ensure

  • Result = not Current.is_odd

is_odd: BOOLEAN

Is Current odd?

ensure

  • Result = not Current.is_even

is_equal (other: MUTABLE_BIG_INTEGER): BOOLEAN

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

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

< (other: MUTABLE_BIG_INTEGER): BOOLEAN

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

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

Create a decimal view of the Current big integer. Note: see also append_in to save memory.

to_unicode_string: UNICODE_STRING

Create a decimal view of the Current big integer. Note: see also append_in_unicode to save memory.

append_in (buffer: STRING)

Append in the buffer the equivalent of to_string. No new STRING creation during the process.

require

  • is_printable

append_in_unicode (buffer: UNICODE_STRING)

Append in the buffer the equivalent of to_string. No new STRING creation during the process.

require

  • is_printable

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

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

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

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

is_printable: BOOLEAN

True if decimal view of Current is short enougth to be put in a STRING.

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.

negate

Negate the sign of Current.

abs

Absolute value of Current.

sign: INTEGER_8

Sign of Current (0 -1 or 1).

set_with_zero

ensure

  • is_zero

hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

copy (other: MUTABLE_BIG_INTEGER)

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

  • same_dynamic_type(other)

ensure

  • is_equal(other)

swap_with (other: MUTABLE_BIG_INTEGER)

Swap the value of Current with the value of other.

storage: NATIVE_ARRAY [E_][INTEGER]

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

Of the allocated storage area.

integer_length: INTEGER

The number of significant INTEGER_32 words in the storage area.

offset: INTEGER

The offset of the less significant word into the storage area.

negative: BOOLEAN

True when Current is negative.

item (index: INTEGER): INTEGER

require

  • index.in_range(offset, offset + integer_length - 1)

put (value: INTEGER, index: INTEGER)

require

  • index.in_range(0, capacity - 1)

set_negative (n: BOOLEAN)

require

  • n implies not is_zero

ensure

  • negative = n or is_zero

set_integer_length (il: INTEGER)

require

  • il.in_range(0, capacity - offset)

ensure

  • integer_length = il

set_offset (o: INTEGER)

require

  • o.in_range(0, capacity - integer_length)

ensure

  • offset = o

set_ilo (il: INTEGER, o: INTEGER)

require

  • il.in_range(0, capacity)
  • o.in_range(0, capacity - il)

ensure

  • integer_length = il
  • offset = o

set_storage (new_storage: NATIVE_ARRAY [E_][INTEGER])
set_capacity (new_capacity: INTEGER)
set_all (new_storage: NATIVE_ARRAY [E_][INTEGER], new_capacity: INTEGER, new_integer_length: INTEGER, new_offset: INTEGER, new_negative: BOOLEAN)

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

  • storage = new_storage
  • capacity = new_capacity
  • integer_length = new_integer_length
  • offset = new_offset
  • negative = new_negative

primitive_shift_left (n: INTEGER_8)

Left shift Current with no need to extend the storage.

require

  • integer_length > 0
  • n.in_range(1, 31)
  • no_bit_lost: item(offset + integer_length - 1) |<< n |>>> n = item(offset + integer_length - 1)

primitive_shift_right (n: INTEGER_8)

Right shift Current of n bits.

require

  • integer_length > 0
  • n.in_range(1, 31)

ensure

  • offset = 0

divide_one_word (divisor: INTEGER): INTEGER

This method is used by divide. The one word divisor is 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)

Correct the value of quotient and remainder after an "unsigned" division. Only used by divide.

require

  • not remainder.is_negative

ensure

  • not remainder.is_negative

divide_sign_correction_bis (other: MUTABLE_BIG_INTEGER, quotient: MUTABLE_BIG_INTEGER, current_negative: BOOLEAN)

Correct the value of quotient and remainder after an "unsigned" division. Only used by divide.

require

  • not is_negative

ensure

  • not is_negative

multiply_and_subtract (u1: INTEGER, qhat: INTEGER, d_storage: NATIVE_ARRAY [E_][INTEGER], d_offset: INTEGER, r_storage: NATIVE_ARRAY [E_][INTEGER], r_offset: INTEGER, length: INTEGER): BOOLEAN

Only used by divide.

require

  • qhat /= 0

add_back (old_u1: INTEGER, d_storage: NATIVE_ARRAY [E_][INTEGER], d_offset: INTEGER, r_storage: NATIVE_ARRAY [E_][INTEGER], r_offset: INTEGER, length: INTEGER): BOOLEAN

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

require

  • other /= Void
  • quotient /= Void
  • remainder /= Void

normalize: INTEGER_8

Shift left until the most significant bit is on. Result give the number of left shift.

require

  • not is_zero

ensure

  • item(offset + integer_length - 1) < 0

register1: MUTABLE_BIG_INTEGER
register2: MUTABLE_BIG_INTEGER
Real_base: REAL
add_magnitude (other: MUTABLE_BIG_INTEGER)

Add the magnitude of Current and other regardless of signs.

require

  • not is_zero
  • not other.is_zero

subtract_magnitude (other: MUTABLE_BIG_INTEGER)

Subtract other from Current (The result is placed in Current) and change negative (the sign) if necessary.

require

  • not is_zero
  • not other.is_zero

subtract_magnitude_raw (other: MUTABLE_BIG_INTEGER)

Subtract (raw) the storage of other from Current. Used by subtract_magnitude.

require

  • not is_zero
  • not other.is_zero
  • abs_compare(other) = 1

ensure

  • offset = 0

subtract_magnitude_raw_reverse (other: MUTABLE_BIG_INTEGER)

Subtract (raw) the storage of Current from other and put it in Current. Used by subtract_magnitude.

require

  • not is_zero
  • not other.is_zero
  • abs_compare(other) = -1

ensure

  • offset = 0

subtract_magnitude_raw_truncated (other: MUTABLE_BIG_INTEGER)

Subtract (raw) the storage of other from Current where other is truncated to the size of Current. Used by subtract_magnitude.

require

  • not other.is_zero
  • other.integer_length >= integer_length
  • unsigned_greater_than(item(offset + integer_length - 1), other.item(offset + integer_length - 1))

ensure

  • offset = 0

subtract_magnitude_raw_reverse_truncated (other: MUTABLE_BIG_INTEGER)

Subtract (raw) the storage of Current from other and put it in Current, where other is truncated to the size of Current. Used by subtract_magnitude.

require

  • not other.is_zero
  • other.integer_length >= integer_length
  • unsigned_less_than(item(offset + integer_length - 1), other.item(offset + integer_length - 1))

ensure

  • offset = 0

char_buffer: FAST_ARRAY [E_][CHARACTER]
append_in_char_buffer: INTEGER

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

  • is_printable
  • not is_zero

capacity_from_lower_bound (actual_capacity: INTEGER, needed_capacity: INTEGER): INTEGER

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, needed_capacity: INTEGER): INTEGER

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, b: INTEGER): BOOLEAN

Unsigned "<".

unsigned_greater_than (a: INTEGER, b: INTEGER): BOOLEAN

Unsigned ">".

unsigned_greater_or_equal (a: INTEGER, b: INTEGER): BOOLEAN

Unsigned ">=".

unsigned_32_to_integer_64 (integer_32: INTEGER): INTEGER_64

Return the unsigned value of the integer_32.

storage_at (s: NATIVE_ARRAY [E_][INTEGER], n: INTEGER): POINTER

Give the address of the corresponding word of s.

mbi_inc (integer_32_adr: POINTER): BOOLEAN

Increment the value at integer_32_adr. The Result is True only in case of overflow.

mbi_add (a: INTEGER, b: INTEGER, integer_32_adr: POINTER): BOOLEAN

t.item(n) := a + b Overflow if "Result = True".

mbi_add_with_inc (a: INTEGER, b: INTEGER, integer_32_adr: POINTER): BOOLEAN

t.item(n) := a + b + 1 Overflow if "Result = True".

mbi_dec (integer_32_adr: POINTER): BOOLEAN

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, b: INTEGER, integer_32_adr: POINTER): BOOLEAN

t.item(n) := a - b Underflow if "Result = True".

mbi_subtract_with_dec (a: INTEGER, b: INTEGER, integer_32_adr: POINTER): BOOLEAN

t.item(n) := a - b - 1 Underflow if "Result = True".

mbi_multiply (a: INTEGER, b: INTEGER, integer_32_adr: POINTER): INTEGER

put a * b in t@n and return the overflow.

mbi_multiply_with_add (a: INTEGER, b: INTEGER, c: INTEGER, integer_32_adr: POINTER): INTEGER

put a * b + c in t@n and return the overflow.

mbi_multiply_with_2_add (a: INTEGER, b: INTEGER, c: INTEGER, d: INTEGER, integer_32_adr: POINTER): INTEGER

put a * b + c + d in t@n and return the overflow.

mbi_divide (u1: INTEGER, u0: INTEGER, d: INTEGER, r_int32adr: POINTER): INTEGER

Divide u1u0 by d, put the remainder in r and return the quotient.

deferred is_equal (other: MUTABLE_BIG_INTEGER): 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: MUTABLE_BIG_INTEGER): 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)

<= (other: MUTABLE_BIG_INTEGER): BOOLEAN

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))

> (other: MUTABLE_BIG_INTEGER): BOOLEAN

Is Current strictly greater than other?

See also <, >=, <=, min, max.

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: MUTABLE_BIG_INTEGER): BOOLEAN

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

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

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

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

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

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

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