home
wiki
classes/clusters list
class information
+
Point of view
MUTABLE_BIG_INTEGER
ANY
MUTABLE_BIG_INTEGER
INTEGER_GENERAL_NUMBER
NUMBER_TOOLS
NUMBER
INTERNALS_HANDLER
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
denominator.is_positive
is_integer_general_number implies denominator.is_one
not is_integer_general_number implies numerator.gcd(denominator) @= 1
Overview
top
creation features
from_native_array
(na:
NATIVE_ARRAY
[
INTEGER_32
], cap:
INTEGER_32
, neg:
BOOLEAN
)
exported features
is_positive
:
BOOLEAN
Is
Current
> 0 ?
is_negative
:
BOOLEAN
Is
Current
< 0 ?
infix "\\"
(other:
NUMBER
):
NUMBER
Remainder of division of
Current
by
other
.
infix "@\\"
(other:
INTEGER_64
):
NUMBER
Remainder of division of
Current
by
other
.
Misc:
hash_code
:
INTEGER_32
The hash-code value of
Current
.
gcd
(other:
NUMBER
):
INTEGER_GENERAL_NUMBER
Great Common Divisor of
Current
and
other
.
is_integer_value
:
BOOLEAN
force_to_real_64
:
REAL_64
Conversion of
Current
in a
REAL_64
.
prefix "-"
:
NUMBER
Opposite of
Current
.
infix "+"
(other:
NUMBER
):
NUMBER
Sum of
Current
and
other
.
infix "//"
(other:
NUMBER
):
NUMBER
Divide
Current
by
other
(Integer division).
infix "@//"
(other:
INTEGER_64
):
NUMBER
Divide
Current
by
other
(Integer division).
infix "*"
(other:
NUMBER
):
NUMBER
Product of
Current
and
other
.
infix "@/"
(other:
INTEGER_64
):
NUMBER
Quotient of
Current
and
other
.
infix "@+"
(other:
INTEGER_64
):
NUMBER
Sum of
Current
and
other
.
infix "@*"
(other:
INTEGER_64
):
NUMBER
inverse
:
NUMBER
infix "@="
(other:
INTEGER_64
):
BOOLEAN
Is
Current
equal
other
?
infix "@<"
(other:
INTEGER_64
):
BOOLEAN
Is
Current
strictly less than
other
?
infix "@>"
(other:
INTEGER_64
):
BOOLEAN
Is
Current
strictly greater than
other
?
infix "@>="
(other:
INTEGER_64
):
BOOLEAN
Is
Current
greater or equal than
other
?
infix "@<="
(other:
INTEGER_64
):
BOOLEAN
Is
Current
less or equal
other
?
comparisons with
NUMBER
infix "<"
(other:
NUMBER
):
BOOLEAN
Is
Current
strictly less than
other
?
comparisons with
REAL_64
infix "#="
(other:
REAL_64
):
BOOLEAN
Is
Current
equal
other
?
infix "#<"
(other:
REAL_64
):
BOOLEAN
Is
Current
strictly less than
other
?
infix "#<="
(other:
REAL_64
):
BOOLEAN
Is
Current
less or equal
other
?
infix "#>"
(other:
REAL_64
):
BOOLEAN
Is
Current
strictly greater than
other
?
infix "#>="
(other:
REAL_64
):
BOOLEAN
Is
Current
greater or equal than
other
?
is_zero
:
BOOLEAN
Is it 0 ?
is_one
:
BOOLEAN
Is it 1 ?
is_equal
(other:
NUMBER
):
BOOLEAN
Compares two LARGE_INTEGERs.
append_in
(buffer:
STRING
)
Append the equivalent of
to_string
at the end of
buffer
.
append_in_unicode
(buffer:
UNICODE_STRING
)
Append the equivalent of
to_unicode_string
at the end of
buffer
.
from_native_array
(na:
NATIVE_ARRAY
[
INTEGER_32
], cap:
INTEGER_32
, neg:
BOOLEAN
)
abs
:
INTEGER_GENERAL_NUMBER
factorial
:
NUMBER
numerator
:
INTEGER_GENERAL_NUMBER
denominator
:
INTEGER_GENERAL_NUMBER
append_decimal_in
(buffer:
STRING
, digits:
INTEGER_32
, all_digits:
BOOLEAN
)
Append the equivalent of
to_decimal
at the end of
buffer
.
Binary operators for two NUMBERs:
infix "-"
(other:
NUMBER
):
NUMBER
Difference of
Current
and
other
.
infix "/"
(other:
NUMBER
):
NUMBER
Quotient of
Current
and
other
.
infix "^"
(exp:
NUMBER
):
NUMBER
Current
raised to
exp
-th power.
infix "<="
(other:
NUMBER
):
BOOLEAN
Is
Current
less or equal than
other
?
infix ">"
(other:
NUMBER
):
BOOLEAN
Is
Current
strictly greater than
other
?
infix ">="
(other:
NUMBER
):
BOOLEAN
Is
Current
greater or equal than
other
?
Unary operators for two NUMBERs:
prefix "+"
:
NUMBER
Unary plus of
Current
.
To know more about a
NUMBER
:
is_integer_8
:
BOOLEAN
Does
Current
value fit on an
INTEGER_8
?
is_integer_16
:
BOOLEAN
Does
Current
value fit on an
INTEGER_16
?
is_integer_32
:
BOOLEAN
Does
Current
value fit on an INTEGER?
is_integer
:
BOOLEAN
is_integer_64
:
BOOLEAN
Does
Current
value fit on an
INTEGER_64
?
in_range
(lower:
NUMBER
, upper:
NUMBER
):
BOOLEAN
Return True if
Current
is in range [
lower
..
upper
]
compare
(other:
NUMBER
):
INTEGER_32
Compare
Current
with
other
.
three_way_comparison
(other:
NUMBER
):
INTEGER_32
Compare
Current
with
other
.
min
(other:
NUMBER
):
NUMBER
Minimum of
Current
and
other
.
max
(other:
NUMBER
):
NUMBER
Maximum of
Current
and
other
.
is_odd
:
BOOLEAN
Is
odd
?
is_even
:
BOOLEAN
Is
even
?
is_integer_general_number
:
BOOLEAN
is_fraction_general_number
:
BOOLEAN
fit_real
:
BOOLEAN
Conversions and printing:
to_integer_8
:
INTEGER_8
Conversion of
Current
in an
INTEGER_8
.
to_integer_16
:
INTEGER_16
Conversion of
Current
in an
INTEGER_16
.
to_integer_32
:
INTEGER_32
Conversion of
Current
in an
INTEGER_32
.
to_integer
:
INTEGER_32
to_integer_64
:
INTEGER_64
Conversion of
Current
in an INTEGER.
to_string
:
STRING
Convert the
NUMBER
into a new allocated
STRING
.
to_unicode_string
:
UNICODE_STRING
Convert the
NUMBER
into a new allocated
UNICODE_STRING
.
to_string_format
(s:
INTEGER_32
):
STRING
Same as
to_string
but the result is on
s
character and the number is right aligned.
to_unicode_string_format
(s:
INTEGER_32
):
UNICODE_STRING
Same as
to_unicode_string
but the result is on
s
character and the number is right aligned.
append_in_format
(str:
STRING
, s:
INTEGER_32
)
Append the equivalent of
to_string_format
at the end of
str
.
append_in_unicode_format
(str:
UNICODE_STRING
, s:
INTEGER_32
)
Append the equivalent of
to_unicode_string_format
at the end of
str
.
to_decimal
(digits:
INTEGER_32
, all_digits:
BOOLEAN
):
STRING
Convert
Current
into its decimal view.
decimal_digit
:
CHARACTER
Gives the corresponding
CHARACTER
for range 0..9.
digit
:
CHARACTER
Gives the corresponding
CHARACTER
for range 0..9.
To mimic
NUMERIC
:
divisible
(other:
NUMBER
):
BOOLEAN
Is
other
a valid divisor for
Current
?
one
:
NUMBER
The neutral element of multiplication.
zero
:
NUMBER
The neutral element of addition.
sign
:
INTEGER_8
Sign of
Current
(0 or -1 or 1).
sqrt
:
REAL_64
Compute the square routine.
log
:
REAL_64
To mix
NUMBER
and
INTEGER_64
:
infix "@-"
(other:
INTEGER_64
):
NUMBER
Difference of
Current
and
other
.
infix "@^"
(exp:
INTEGER_64
):
NUMBER
Misc:
out_in_tagged_out_memory
Append terse printable represention of current object in
tagged_out_memory
.
fill_tagged_out_memory
Append a viewable information in
tagged_out_memory
in order to affect the behavior of
out
,
tagged_out
, etc.
is_positive
:
BOOLEAN
effective function
top
Is
Current
> 0 ?
ensure
Result = Current @> 0
is_negative
:
BOOLEAN
effective function
top
Is
Current
< 0 ?
ensure
Result = Current @< 0
infix "\\"
(other:
NUMBER
):
NUMBER
effective function
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
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
top
The hash-code value of
Current
.
ensure
good_hash_value:
Result >= 0
gcd
(other:
NUMBER
):
INTEGER_GENERAL_NUMBER
effective function
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
constant attribute
top
force_to_real_64
:
REAL_64
effective function
top
Conversion of
Current
in a
REAL_64
.
require
fit_real
prefix "-"
:
NUMBER
effective function
top
Opposite of
Current
.
ensure
Result /= Void
infix "+"
(other:
NUMBER
):
NUMBER
effective function
top
Sum of
Current
and
other
.
require
other /= Void
ensure
Result - other.is_equal(Current)
infix "//"
(other:
NUMBER
):
NUMBER
effective function
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
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
top
Product of
Current
and
other
.
require
other /= Void
ensure
Result /= Void
infix "@/"
(other:
INTEGER_64
):
NUMBER
effective function
top
Quotient of
Current
and
other
.
require
other /= 0
ensure
Result /= Void
infix "@+"
(other:
INTEGER_64
):
NUMBER
effective function
top
Sum of
Current
and
other
.
ensure
Result /= Void
infix "@*"
(other:
INTEGER_64
):
NUMBER
effective function
top
ensure
Result /= Void
inverse
:
NUMBER
effective function
top
require
divisible(Current)
ensure
Result /= Void
infix "@="
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
equal
other
?
infix "@<"
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
strictly less than
other
?
ensure
Result = not Current @>= other
infix "@>"
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
strictly greater than
other
?
ensure
Result = not Current @<= other
infix "@>="
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
greater or equal than
other
?
ensure
Result = not Current @< other
infix "@<="
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
less or equal
other
?
ensure
Result = not Current @> other
infix "<"
(other:
NUMBER
):
BOOLEAN
effective function
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
top
Is
Current
equal
other
?
infix "#<"
(other:
REAL_64
):
BOOLEAN
effective function
top
Is
Current
strictly less than
other
?
ensure
Result implies not Current #>= other
infix "#<="
(other:
REAL_64
):
BOOLEAN
effective function
top
Is
Current
less or equal
other
?
ensure
Result = not Current #> other
infix "#>"
(other:
REAL_64
):
BOOLEAN
effective function
top
Is
Current
strictly greater than
other
?
ensure
Result = not Current #<= other
infix "#>="
(other:
REAL_64
):
BOOLEAN
effective function
top
Is
Current
greater or equal than
other
?
ensure
Result = not Current #< other
is_zero
:
BOOLEAN
constant attribute
top
Is it 0 ?
ensure
Result = Current @= 0
is_one
:
BOOLEAN
constant attribute
top
Is it 1 ?
ensure
Result = Current @= 1
is_equal
(other:
NUMBER
):
BOOLEAN
effective function
top
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)
Result implies hash_code = other.hash_code
trichotomy:
Result = not Current < other and not other < Current
append_in
(buffer:
STRING
)
effective procedure
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
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
from_native_array
(na:
NATIVE_ARRAY
[
INTEGER_32
], cap:
INTEGER_32
, neg:
BOOLEAN
)
effective procedure
top
abs
:
INTEGER_GENERAL_NUMBER
effective function
top
ensure
not Result.is_negative
factorial
:
NUMBER
effective function
top
require
is_integer_general_number
not is_negative
ensure
Result.is_integer_general_number
Result.is_positive
numerator
:
INTEGER_GENERAL_NUMBER
effective function
top
denominator
:
INTEGER_GENERAL_NUMBER
effective function
top
append_decimal_in
(buffer:
STRING
, digits:
INTEGER_32
, all_digits:
BOOLEAN
)
effective procedure
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
infix "-"
(other:
NUMBER
):
NUMBER
effective function
top
Difference of
Current
and
other
.
require
other /= Void
ensure
Result
+
other.
is_equal
(Current)
infix "/"
(other:
NUMBER
):
NUMBER
effective function
top
Quotient of
Current
and
other
.
require
other /= Void
divisible(other)
ensure
Result /= Void
infix "^"
(exp:
NUMBER
):
NUMBER
effective function
top
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
infix "<="
(other:
NUMBER
):
BOOLEAN
effective function
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
top
Is
Current
strictly greater than
other
?
require
other_exists:
other /= Void
ensure
definition:
Result = other < Current
infix ">="
(other:
NUMBER
):
BOOLEAN
effective function
top
Is
Current
greater or equal than
other
?
require
other_exists:
other /= Void
ensure
definition:
Result = other <= Current
prefix "+"
:
NUMBER
frozen
effective function
top
Unary plus of
Current
.
ensure
Result = Current
is_integer_8
:
BOOLEAN
frozen
effective function
top
Does
Current
value fit on an
INTEGER_8
?
ensure
Result implies
is_integer_general_number
is_integer_16
:
BOOLEAN
frozen
effective function
top
Does
Current
value fit on an
INTEGER_16
?
ensure
Result implies
is_integer_general_number
is_integer_32
:
BOOLEAN
frozen
effective function
top
Does
Current
value fit on an INTEGER?
ensure
Result implies
is_integer_general_number
is_integer
:
BOOLEAN
frozen
effective function
top
This feature is obsolete:
Now use `is_integer_32' instead (march 2006).
is_integer_64
:
BOOLEAN
frozen
effective function
top
Does
Current
value fit on an
INTEGER_64
?
ensure
Result implies
is_integer_general_number
in_range
(lower:
NUMBER
, upper:
NUMBER
):
BOOLEAN
effective function
top
Return True if
Current
is in range [
lower
..
upper
]
ensure
Result = Current >= lower and Current <= upper
compare
(other:
NUMBER
):
INTEGER_32
effective function
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
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
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
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
top
Is
odd
?
require
is_integer_general_number
is_even
:
BOOLEAN
effective function
top
Is
even
?
require
is_integer_general_number
is_integer_general_number
:
BOOLEAN
frozen
effective function
top
is_fraction_general_number
:
BOOLEAN
frozen
effective function
top
fit_real
:
BOOLEAN
frozen
effective function
top
to_integer_8
:
INTEGER_8
frozen
effective function
top
Conversion of
Current
in an
INTEGER_8
.
require
is_integer_8
to_integer_16
:
INTEGER_16
frozen
effective function
top
Conversion of
Current
in an
INTEGER_16
.
require
is_integer_16
to_integer_32
:
INTEGER_32
frozen
effective function
top
Conversion of
Current
in an
INTEGER_32
.
require
is_integer_32
to_integer
:
INTEGER_32
frozen
effective function
top
This feature is obsolete:
Now use `to_integer_32' instead (march 2006).
to_integer_64
:
INTEGER_64
frozen
effective function
top
Conversion of
Current
in an INTEGER.
require
is_integer_64
to_string
:
STRING
frozen
effective function
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
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
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
to_string
.count <= s
ensure
Result.count = s
to_unicode_string_format
(s:
INTEGER_32
):
UNICODE_STRING
frozen
effective function
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
to_string
.count <= s
ensure
Result.count = s
append_in_format
(str:
STRING
, s:
INTEGER_32
)
frozen
effective procedure
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
to_string
.count <= s
ensure
str.count >= old str.count + s
append_in_unicode_format
(str:
UNICODE_STRING
, s:
INTEGER_32
)
frozen
effective procedure
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
to_string
.count <= s
ensure
str.count >= old str.count + s
to_decimal
(digits:
INTEGER_32
, all_digits:
BOOLEAN
):
STRING
frozen
effective function
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
top
Gives the corresponding
CHARACTER
for range 0..9.
require
to_integer_32
.in_range(0, 9)
ensure
"0123456789".has(Result)
Current
@=
Result.value
digit
:
CHARACTER
effective function
top
Gives the corresponding
CHARACTER
for range 0..9.
require
to_integer_32
.in_range(0, 9)
ensure
"0123456789".has(Result)
Current
@=
Result.value
divisible
(other:
NUMBER
):
BOOLEAN
effective function
top
Is
other
a valid divisor for
Current
?
require
other /= Void
one
:
NUMBER
once function
top
The neutral element of multiplication.
zero
:
NUMBER
once function
top
The neutral element of addition.
sign
:
INTEGER_8
frozen
effective function
top
Sign of
Current
(0 or -1 or 1).
ensure
Result = 1 implies
is_positive
Result = 0 implies
is_zero
Result = -1 implies
is_negative
Result.in_range(-1, 1)
sqrt
:
REAL_64
effective function
top
Compute the square routine.
require
fit_real
log
:
REAL_64
frozen
effective function
top
require
fit_real
infix "@-"
(other:
INTEGER_64
):
NUMBER
effective function
top
Difference of
Current
and
other
.
ensure
Result /= Void
infix "@^"
(exp:
INTEGER_64
):
NUMBER
effective function
top
require
is_zero
implies exp > 0
ensure
Result /= Void
out_in_tagged_out_memory
effective procedure
top
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
effective procedure
top
Append a viewable information in
tagged_out_memory
in order to affect the behavior of
out
,
tagged_out
, etc.