+
Point of view
All features
class BIG_INTEGER_NUMBER
Summary
top
To implement NUMBER (do not use this class, see NUMBER).
Direct parents
Inherit list: INTEGER_GENERAL_NUMBER
Class invariant
top
Overview
top
Creation features
{ANY}
Features
{ANY}
Misc:
{ANY}
{NUMBER}
Multiplication
{NUMBER}
division
{NUMBER}
Implementation:
{NUMBER}
{ANY}
comparisons with NUMBER
{ANY}
comparisons with REAL_64
{ANY}
{NUMBER, NUMBER_TOOLS}
{ANY}
{NUMBER}
{MUTABLE_BIG_INTEGER}
{NUMBER}
{}
{ANY}
{ANY}
Implementation:
{NUMBER}
{INTEGER_GENERAL_NUMBER}
Binary operators for two NUMBERs:
{ANY}
Unary operators for two NUMBERs:
{ANY}
To know more about a NUMBER:
{ANY}
Conversions and printing:
{ANY}
To mimic NUMERIC:
{ANY}
To mix NUMBER and INTEGER_64:
{ANY}
Misc:
{ANY}
Implementation:
{NUMBER}
{NUMBER, NUMBER_TOOLS}
To implement efficient calculus
{NUMBER}
{}
To create fractions
{}
{ANY}
  • bounded_by (a_min: BIG_INTEGER_NUMBER, a_max: BIG_INTEGER_NUMBER): BIG_INTEGER_NUMBER
    A value that is equal to Current if it is between the limits set by a_min and a_max.
Maximum:
{}
Minimum:
{}
Bits:
{}
is_positive: BOOLEAN
effective function
{ANY}
top
Is Current > 0 ?
ensure
  • Result = Current @> 0
is_negative: BOOLEAN
effective function
{ANY}
top
Is Current < 0 ?
ensure
  • Result = Current @< 0
infix "\\" (other: NUMBER): NUMBER
effective function
{ANY}
top
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
infix "@\\" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
Remainder of division of Current by other.
require
  • is_integer_general_number
  • other /= 0
ensure
  • Result.is_integer_general_number
hash_code: INTEGER_32
effective function
{ANY}
top
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
effective function
{ANY}
top
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
is False
constant attribute
{ANY}
top
force_to_real_64: REAL_64
effective function
{ANY}
top
Conversion of Current in a REAL_64.
require
  • fit_real
prefix "-": NUMBER
effective function
{ANY}
top
Opposite of Current.
ensure
  • Result /= Void
infix "+" (other: NUMBER): NUMBER
effective function
{ANY}
top
Sum of Current and other.
require
  • other /= Void
ensure
  • Result - other.is_equal(Current)
infix "//" (other: NUMBER): NUMBER
effective function
{ANY}
top
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)
infix "@//" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
Divide Current by other (Integer division).
require
  • is_integer_general_number
  • other /= 0
ensure
  • Result.is_integer_general_number
infix "*" (other: NUMBER): NUMBER
effective function
{ANY}
top
Product of Current and other.
require
  • other /= Void
ensure
  • Result /= Void
infix "@/" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
Quotient of Current and other.
require
  • other /= 0
ensure
  • Result /= Void
infix "@+" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
Sum of Current and other.
ensure
  • Result /= Void
infix "@*" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
ensure
  • Result /= Void
add_with_big_integer_number (other: BIG_INTEGER_NUMBER): NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
add_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
multiply_with_big_integer_number (other: BIG_INTEGER_NUMBER): NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
multiply_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
integer_divide_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
remainder_of_divide_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
integer_divide_big_integer_number (other: BIG_INTEGER_NUMBER): INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
remainder_of_divide_big_integer_number (other: BIG_INTEGER_NUMBER): INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
gcd_with_integer_64_number (other: INTEGER_64_NUMBER): INTEGER_GENERAL_NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
inverse: NUMBER
effective function
{ANY}
top
require
  • divisible(Current)
ensure
  • Result /= Void
infix "@=" (other: INTEGER_64): BOOLEAN
effective function
{ANY}
top
Is Current equal other ?
infix "@<" (other: INTEGER_64): BOOLEAN
effective function
{ANY}
top
Is Current strictly less than other?
ensure
  • Result = not Current @>= other
infix "@>" (other: INTEGER_64): BOOLEAN
effective function
{ANY}
top
Is Current strictly greater than other?
ensure
  • Result = not Current @<= other
infix "@>=" (other: INTEGER_64): BOOLEAN
effective function
{ANY}
top
Is Current greater or equal than other?
ensure
  • Result = not Current @< other
infix "@<=" (other: INTEGER_64): BOOLEAN
effective function
{ANY}
top
Is Current less or equal other?
ensure
  • Result = not Current @> other
infix "<" (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Is Current strictly less than other?
require
  • other_exists: other /= Void
ensure
  • asymmetric: Result implies not other < Current
infix "#=" (other: REAL_64): BOOLEAN
effective function
{ANY}
top
Is Current equal other?
infix "#<" (other: REAL_64): BOOLEAN
effective function
{ANY}
top
Is Current strictly less than other?
ensure
  • Result implies not Current #>= other
infix "#<=" (other: REAL_64): BOOLEAN
effective function
{ANY}
top
Is Current less or equal other?
ensure
  • Result = not Current #> other
infix "#>" (other: REAL_64): BOOLEAN
effective function
{ANY}
top
Is Current strictly greater than other?
ensure
  • Result = not Current #<= other
infix "#>=" (other: REAL_64): BOOLEAN
effective function
{ANY}
top
Is Current greater or equal than other?
ensure
  • Result = not Current #< other
greater_with_big_integer_number (other: BIG_INTEGER_NUMBER): BOOLEAN
effective function
{NUMBER, NUMBER_TOOLS}
top
require
  • other /= Void
greater_with_fraction_with_big_integer_number (other: FRACTION_WITH_BIG_INTEGER_NUMBER): BOOLEAN
effective function
{NUMBER, NUMBER_TOOLS}
top
require
  • other /= Void
is_zero: BOOLEAN
is False
constant attribute
{ANY}
top
Is it 0 ?
ensure
  • Result = Current @= 0
is_one: BOOLEAN
is False
constant attribute
{ANY}
top
Is it 1 ?
ensure
  • Result = Current @= 1
is_equal (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Compares two LARGE_INTEGERs.
As they both have same sign comparison is done with absolute values.
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
append_in (buffer: STRING)
effective procedure
{ANY}
top
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)
effective procedure
{ANY}
top
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
effective function
{NUMBER}
top
ensure
value_length: INTEGER_32
effective function
{NUMBER}
top
ensure
from_native_array (na: NATIVE_ARRAY[INTEGER_32], cap: INTEGER_32, neg: BOOLEAN)
effective procedure
{MUTABLE_BIG_INTEGER}
top
ensure
put_into_mutable_big_integer (mut: MUTABLE_BIG_INTEGER)
effective procedure
{NUMBER}
top
require
  • mut /= Void
ensure
  • mut.to_integer_general_number.is_equal(Current)
is_natural_64_: BOOLEAN
effective function
{NUMBER}
top
to_natural_64_: NATURAL_64
effective function
{NUMBER}
top
signed_32_to_unsigned_64 (integer_32: INTEGER_32): NATURAL_64
{}
top
negative: BOOLEAN
writable attribute
{}
top
capacity: INTEGER_32
writable attribute
{}
top
writable attribute
{}
top
effective function
{ANY}
top
ensure
  • not Result.is_negative
factorial: NUMBER
effective function
{ANY}
top
require
  • is_integer_general_number
  • not is_negative
ensure
  • Result.is_integer_general_number
  • Result.is_positive
effective function
{ANY}
top
effective function
{ANY}
top
append_decimal_in (buffer: STRING, digits: INTEGER_32, all_digits: BOOLEAN)
effective procedure
{ANY}
top
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
effective function
{NUMBER}
top
require
  • other /= Void
integer_general_number_zero: INTEGER_GENERAL_NUMBER
once function
{INTEGER_GENERAL_NUMBER}
top
ensure
integer_general_number_one: INTEGER_GENERAL_NUMBER
once function
{INTEGER_GENERAL_NUMBER}
top
ensure
integer_general_number_one_negative: INTEGER_GENERAL_NUMBER
once function
{INTEGER_GENERAL_NUMBER}
top
ensure
  • - Result.is_one
infix "-" (other: NUMBER): NUMBER
effective function
{ANY}
top
Difference of Current and other.
require
  • other /= Void
ensure
infix "/" (other: NUMBER): NUMBER
effective function
{ANY}
top
Quotient of Current and other.
require
  • other /= Void
  • other /= zero
  • divisible(other)
ensure
  • Result /= Void
infix "^" (exp: NUMBER): NUMBER
effective function
{ANY}
top
Current raised to exp-th power.
require ensure
infix "<=" (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Is Current less or equal than other?
require
  • other_exists: other /= Void
ensure
  • definition: Result = Current < other or is_equal(other)
infix ">" (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Is Current strictly greater than other?
require
  • other_exists: other /= Void
ensure
  • definition: Result = other < Current
infix ">=" (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Is Current greater or equal than other?
require
  • other_exists: other /= Void
ensure
  • definition: Result = other <= Current
prefix "+": NUMBER
frozen
effective function
{ANY}
top
Unary plus of Current.
ensure
  • Result = Current
is_integer_8: BOOLEAN
frozen
effective function
{ANY}
top
Does Current value fit on an INTEGER_8?
ensure
is_integer_16: BOOLEAN
frozen
effective function
{ANY}
top
Does Current value fit on an INTEGER_16?
ensure
is_integer_32: BOOLEAN
frozen
effective function
{ANY}
top
Does Current value fit on an INTEGER?
ensure
is_integer_64: BOOLEAN
frozen
effective function
{ANY}
top
Does Current value fit on an INTEGER_64?
ensure
is_natural_64: BOOLEAN
frozen
effective function
{ANY}
top
Does Current value fit on a NATURAL_64?
ensure
in_range (lower: NUMBER, upper: NUMBER): BOOLEAN
effective function
{ANY}
top
Return True if Current is in range [lower..upper]
ensure
  • Result = Current >= lower and Current <= upper
compare (other: NUMBER): INTEGER_32
effective function
{ANY}
top
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_32
effective function
{ANY}
top
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
effective function
{ANY}
top
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
effective function
{ANY}
top
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
effective function
{ANY}
top
Is odd ?
is_even: BOOLEAN
effective function
{ANY}
top
Is even ?
is_integer_general_number: BOOLEAN
frozen
effective function
{ANY}
top
is_fraction_general_number: BOOLEAN
frozen
effective function
{ANY}
top
fit_real: BOOLEAN
frozen
effective function
{ANY}
top
to_integer_8: INTEGER_8
frozen
effective function
{ANY}
top
Conversion of Current in an INTEGER_8.
require
to_integer_16: INTEGER_16
frozen
effective function
{ANY}
top
Conversion of Current in an INTEGER_16.
require
to_integer_32: INTEGER_32
frozen
effective function
{ANY}
top
Conversion of Current in an INTEGER_32.
require
to_integer_64: INTEGER_64
frozen
effective function
{ANY}
top
Conversion of Current in an INTEGER.
require
to_natural_64: NATURAL_64
frozen
effective function
{ANY}
top
Conversion of Current in a NATURAL_64.
require
to_string: STRING
frozen
effective function
{ANY}
top
Convert the NUMBER into a new allocated STRING.
Note: see also append_in to save memory.
to_unicode_string: UNICODE_STRING
frozen
effective function
{ANY}
top
Convert the NUMBER into a new allocated UNICODE_STRING.
Note: see also append_in_unicode to save memory.
to_string_format (s: INTEGER_32): STRING
frozen
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
frozen
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)
frozen
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)
frozen
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
to_decimal (digits: INTEGER_32, all_digits: BOOLEAN): STRING
frozen
effective function
{ANY}
top
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
decimal_digit: CHARACTER
frozen
effective function
{ANY}
top
Gives the corresponding CHARACTER for range 0..9.
require ensure
  • "0123456789".has(Result)
  • Current @= Result.value
digit: CHARACTER
effective function
{ANY}
top
Gives the corresponding CHARACTER for range 0..9.
require ensure
  • "0123456789".has(Result)
  • Current @= Result.value
divisible (other: NUMBER): BOOLEAN
effective function
{ANY}
top
Is other a valid divisor for Current ?
require
  • other /= Void
one: NUMBER
once function
{ANY}
top
The neutral element of multiplication.
zero: NUMBER
once function
{ANY}
top
The neutral element of addition.
sign: INTEGER_8
frozen
effective function
{ANY}
top
Sign of Current (0 or -1 or 1).
ensure
sqrt: REAL_64
effective function
{ANY}
top
Compute the square routine.
require
log: REAL_64
frozen
effective function
{ANY}
top
require
infix "@-" (other: INTEGER_64): NUMBER
effective function
{ANY}
top
Difference of Current and other.
ensure
  • Result /= Void
infix "@^" (exp: INTEGER_64): NUMBER
effective function
{ANY}
top
require ensure
  • Result /= Void
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
add_with_integer_64_number (other: INTEGER_64_NUMBER): NUMBER
frozen
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
multiply_with_integer_64_number (other: INTEGER_64_NUMBER): NUMBER
effective function
{NUMBER}
top
require
  • other /= Void
ensure
  • Result /= Void
greater_with_integer_64_number (other: INTEGER_64_NUMBER): BOOLEAN
effective function
{NUMBER}
top
require
  • other /= Void
max_double: NUMBER
once function
{NUMBER, NUMBER_TOOLS}
top
min_double: NUMBER
once function
{NUMBER, NUMBER_TOOLS}
top
mutable_register1: MUTABLE_BIG_INTEGER
once function
{NUMBER}
top
mutable_register2: MUTABLE_BIG_INTEGER
once function
{NUMBER}
top
mutable_register3: MUTABLE_BIG_INTEGER
once function
{NUMBER}
top
mutable_register4: MUTABLE_BIG_INTEGER
once function
{NUMBER}
top
string_buffer: STRING
once function
{}
top
unicode_string_buffer: UNICODE_STRING
once function
{}
top
from_two_integer (n: INTEGER_64, d: INTEGER_64): NUMBER
effective function
{}
top
require
  • d /= 0
ensure
from_two_integer_general_number (n: INTEGER_GENERAL_NUMBER, d: INTEGER_GENERAL_NUMBER): NUMBER
effective function
{}
top
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
effective function
{}
top
require
  • d /= Void
  • not d.is_zero
from_integer_general_number_and_integer (n: INTEGER_GENERAL_NUMBER, d: INTEGER_64): NUMBER
effective function
{}
top
require
  • n /= Void
  • d /= 0
bounded_by (a_min: BIG_INTEGER_NUMBER, a_max: BIG_INTEGER_NUMBER): BIG_INTEGER_NUMBER
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.