home
wiki
classes/clusters list
class information
+
Point of view
All features
ANY
NUMBER_TOOLS
NUMBER
INTERNALS_HANDLER
All features
class FRACTION_WITH_BIG_INTEGER_NUMBER
Summary
top
To implement
NUMBER
(do not use this class, see
NUMBER
).
Direct parents
inherit list:
FRACTION_GENERAL_NUMBER
Class invariant
top
denominator @>= 2
not numerator.is_zero
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
make
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
Create a simplified large_fraction
make_simply
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
create a large_fraction without simplify it
features
numerator
:
INTEGER_GENERAL_NUMBER
denominator
:
INTEGER_GENERAL_NUMBER
make
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
Create a simplified large_fraction
make_simply
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
create a large_fraction without simplify it
inverse
:
NUMBER
prefix "-"
:
NUMBER
Opposite of
Current
.
infix "+"
(other:
NUMBER
):
NUMBER
Sum of
Current
and
other
.
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
.
append_decimal_in
(buffer:
STRING
, digits:
INTEGER_32
, all_digits:
BOOLEAN
)
Append the equivalent of
to_decimal
at the end of
buffer
.
is_equal
(other:
NUMBER
):
BOOLEAN
Is
other
attached to an object considered equal to current object?
force_to_real_64
:
REAL_64
infix "*"
(other:
NUMBER
):
NUMBER
Product of
Current
and
other
.
infix "@+"
(other:
INTEGER_64
):
NUMBER
Sum of 'Current' and 'other'.
add_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
NUMBER
add_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
NUMBER
multiply_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
NUMBER
multiply_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
NUMBER
infix "@*"
(other:
INTEGER_64
):
NUMBER
infix "@/"
(other:
INTEGER_64
):
NUMBER
Quotient of
Current
and
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
less or equal
other
?
infix "@>="
(other:
INTEGER_64
):
BOOLEAN
Is
Current
greater or equal than
other
?
infix "<"
(other:
NUMBER
):
BOOLEAN
Is
Current
strictly less than
other
?
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
greater or equal than
other
?
infix "#>"
(other:
REAL_64
):
BOOLEAN
Is
Current
strictly greater than
other
?
greater_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
BOOLEAN
greater_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
BOOLEAN
is_zero
:
BOOLEAN
Is it 0 ?
is_one
:
BOOLEAN
Is it 1 ?
is_positive
:
BOOLEAN
Is
Current
> 0 ?
is_negative
:
BOOLEAN
Is
Current
< 0 ?
factorial
:
NUMBER
infix "@="
(other:
INTEGER_64
):
BOOLEAN
Is
Current
equal
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
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
.
decimal_in
(buffer:
STRING
, num:
NUMBER
, denom:
NUMBER
, negative:
BOOLEAN
, digits:
INTEGER_32
, all_digits:
BOOLEAN
)
Implementation:
gcd_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
INTEGER_GENERAL_NUMBER
gcd_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
INTEGER_GENERAL_NUMBER
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
abs
:
NUMBER
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.
Implementation:
add_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
NUMBER
multiply_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
NUMBER
greater_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
BOOLEAN
max_double
:
NUMBER
min_double
:
NUMBER
To implement efficient calculus
mutable_register1
:
MUTABLE_BIG_INTEGER
mutable_register2
:
MUTABLE_BIG_INTEGER
mutable_register3
:
MUTABLE_BIG_INTEGER
mutable_register4
:
MUTABLE_BIG_INTEGER
string_buffer
:
STRING
unicode_string_buffer
:
UNICODE_STRING
To create fractions
from_two_integer
(n:
INTEGER_64
, d:
INTEGER_64
):
NUMBER
from_two_integer_general_number
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
):
NUMBER
from_integer_and_integer_general_number
(n:
INTEGER_64
, d:
INTEGER_GENERAL_NUMBER
):
NUMBER
from_integer_general_number_and_integer
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_64
):
NUMBER
Maximum:
Maximum_character_code
:
INTEGER_16
Largest supported code for
CHARACTER
values.
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_32
Largest supported value of type INTEGER/
INTEGER_32
.
Maximum_integer_32
:
INTEGER_32
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_64
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Maximum_real_64
:
REAL_64
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Maximum_real_80
:
REAL_EXTENDED
Largest supported value of type
REAL_80
.
Minimum:
Minimum_character_code
:
INTEGER_16
Smallest supported code for
CHARACTER
values.
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_32
Smallest supported value of type INTEGER/
INTEGER_32
.
Minimum_integer_32
:
INTEGER_32
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_64
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Minimum_real_64
:
REAL_64
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Minimum_real_80
:
REAL_64
Smallest supported value of type
REAL_80
.
Bits:
Boolean_bits
:
INTEGER_32
Number of bits in a value of type
BOOLEAN
.
Character_bits
:
INTEGER_32
Number of bits in a value of type
CHARACTER
.
Integer_bits
:
INTEGER_32
Number of bits in a value of type INTEGER.
Real_bits
:
INTEGER_32
Number of bits in a value of type REAL.
Pointer_bits
:
INTEGER_32
Number of bits in a value of type
POINTER
.
numerator
:
INTEGER_GENERAL_NUMBER
writable attribute
top
denominator
:
INTEGER_GENERAL_NUMBER
writable attribute
top
make
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
effective procedure
top
Create a simplified large_fraction
require
not n \\ d @= 0
make_simply
(n:
INTEGER_GENERAL_NUMBER
, d:
INTEGER_GENERAL_NUMBER
)
effective procedure
top
create a large_fraction without simplify it
require
d.is_positive
n.gcd(d).is_one
d @>= 2
ensure
numerator
= n
denominator
= d
inverse
:
NUMBER
effective function
top
require
divisible(Current)
ensure
Result /= Void
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)
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
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
is_equal
(other:
NUMBER
):
BOOLEAN
effective function
top
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)
Result implies hash_code = other.hash_code
trichotomy:
Result = not Current < other and not other < Current
force_to_real_64
:
REAL_64
effective function
top
require
fit_real
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
Sum of 'Current' and 'other'.
ensure
Result /= Void
add_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
NUMBER
effective function
top
require
other /= Void
ensure
Result /= Void
add_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
NUMBER
effective function
top
require
other /= Void
ensure
Result /= Void
multiply_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
NUMBER
effective function
top
require
other /= Void
ensure
Result /= Void
multiply_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
NUMBER
effective function
top
require
other /= Void
ensure
Result /= Void
infix "@*"
(other:
INTEGER_64
):
NUMBER
effective function
top
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
):
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
less or equal
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:
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
greater or equal than
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
greater_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
BOOLEAN
effective function
top
require
other /= Void
greater_with_fraction_with_big_integer_number
(other: FRACTION_WITH_BIG_INTEGER_NUMBER):
BOOLEAN
effective function
top
require
other /= Void
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_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
factorial
:
NUMBER
effective function
top
require
is_integer_general_number
not is_negative
ensure
Result.is_integer_general_number
Result.is_positive
infix "@="
(other:
INTEGER_64
):
BOOLEAN
effective function
top
Is
Current
equal
other
?
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
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
decimal_in
(buffer:
STRING
, num:
NUMBER
, denom:
NUMBER
, negative:
BOOLEAN
, digits:
INTEGER_32
, all_digits:
BOOLEAN
)
effective procedure
top
gcd_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
INTEGER_GENERAL_NUMBER
effective function
top
require
other /= Void
gcd_with_big_integer_number
(other:
BIG_INTEGER_NUMBER
):
INTEGER_GENERAL_NUMBER
effective function
top
require
other /= Void
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
abs
:
NUMBER
effective function
top
ensure
not Result.
is_negative
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.
add_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
NUMBER
frozen
effective function
top
require
other /= Void
ensure
Result /= Void
multiply_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
NUMBER
effective function
top
require
other /= Void
ensure
Result /= Void
greater_with_integer_64_number
(other:
INTEGER_64_NUMBER
):
BOOLEAN
effective function
top
require
other /= Void
max_double
:
NUMBER
once function
top
min_double
:
NUMBER
once function
top
mutable_register1
:
MUTABLE_BIG_INTEGER
once function
top
mutable_register2
:
MUTABLE_BIG_INTEGER
once function
top
mutable_register3
:
MUTABLE_BIG_INTEGER
once function
top
mutable_register4
:
MUTABLE_BIG_INTEGER
once function
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
Result
@*
d
@=
n
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
Maximum_character_code
:
INTEGER_16
top
Largest supported code for
CHARACTER
values.
ensure
meaningful:
Result >= 127
Maximum_integer_8
:
INTEGER_8
constant attribute
top
Largest supported value of type
INTEGER_8
.
Maximum_integer_16
:
INTEGER_16
constant attribute
top
Largest supported value of type
INTEGER_16
.
Maximum_integer
:
INTEGER_32
constant attribute
top
Largest supported value of type INTEGER/
INTEGER_32
.
Maximum_integer_32
:
INTEGER_32
constant attribute
top
Largest supported value of type INTEGER/
INTEGER_32
.
Maximum_integer_64
:
INTEGER_64
constant attribute
top
Largest supported value of type
INTEGER_64
.
Maximum_real_32
:
REAL_32
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
meaningful:
Result >=
Maximum_real
Minimum_character_code
:
INTEGER_16
top
Smallest supported code for
CHARACTER
values.
ensure
meaningful:
Result <= 0
Minimum_integer_8
:
INTEGER_8
constant attribute
top
Smallest supported value of type
INTEGER_8
.
Minimum_integer_16
:
INTEGER_16
constant attribute
top
Smallest supported value of type
INTEGER_16
.
Minimum_integer
:
INTEGER_32
constant attribute
top
Smallest supported value of type INTEGER/
INTEGER_32
.
Minimum_integer_32
:
INTEGER_32
constant attribute
top
Smallest supported value of type INTEGER/
INTEGER_32
.
Minimum_integer_64
:
INTEGER_64
constant attribute
top
Smallest supported value of type
INTEGER_64
.
Minimum_real_32
:
REAL_32
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
meaningful:
Result >= 1
large_enough:
{INTEGER_32 2} ^ Result >=
Maximum_character_code
Integer_bits
:
INTEGER_32
top
Number of bits in a value of type INTEGER.
ensure
integer_definition:
Result = 32
Real_bits
:
INTEGER_32
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
.