deferred class FRACTION_GENERAL_NUMBER

Features exported to ANY

To implement NUMBER (do not use this class, see NUMBER).

Direct parents

conformant parents

NUMBER

Known children

conformant children

FRACTION_WITH_BIG_INTEGER_NUMBER

Summary

exported features

Misc:

Binary operators for two NUMBERs:

Unary operators for two NUMBERs:

To know more about a NUMBER:

Conversions and printing:

To mimic NUMERIC:

To mix NUMBER and INTEGER_64:

To mix NUMBER and REAL_64:

Misc:

Details

is_zero: BOOLEAN

Is it 0 ?

ensure

  • Result = Current @= 0

is_one: BOOLEAN

Is it 1 ?

ensure

  • Result = Current @= 1

is_positive: BOOLEAN

Is Current > 0 ?

ensure

  • Result = Current @> 0

is_negative: BOOLEAN

Is Current < 0 ?

ensure

  • Result = Current @< 0

factorial: NUMBER

require

  • is_integer_general_number
  • not is_negative

ensure

  • Result.is_integer_general_number
  • Result.is_positive

@= (other: INTEGER_64): BOOLEAN

Is Current equal other ?

// (other: NUMBER): NUMBER

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)

@// (other: INTEGER_64): NUMBER

Divide Current by other (Integer division).

require

  • is_integer_general_number
  • other /= 0

ensure

  • Result.is_integer_general_number

\\ (other: NUMBER): NUMBER

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

@\\ (other: INTEGER_64): NUMBER

Remainder of division of Current by other.

require

  • is_integer_general_number
  • other /= 0

ensure

  • Result.is_integer_general_number

hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

gcd (other: NUMBER): INTEGER_GENERAL_NUMBER

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

deferred + (other: NUMBER): NUMBER

Sum of Current and other.

require

  • other /= Void

ensure

  • (Result - other).is_equal(Current)

- (other: NUMBER): NUMBER

Difference of Current and other.

require

  • other /= Void

ensure

  • (Result + other).is_equal(Current)

deferred * (other: NUMBER): NUMBER

Product of Current and other.

require

  • other /= Void

ensure

  • Result /= Void

/ (other: NUMBER): NUMBER

Quotient of Current and other.

require

  • other /= Void
  • divisible(other)

ensure

  • Result /= Void

^ (exp: NUMBER): NUMBER

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

deferred < (other: NUMBER): BOOLEAN

Is Current strictly less than other?

require

  • other_exists: other /= Void

ensure

  • asymmetric: Result implies not (other < Current)

<= (other: NUMBER): BOOLEAN

Is Current less or equal than other?

require

  • other_exists: other /= Void

ensure

  • definition: Result = (Current < other or is_equal(other))

> (other: NUMBER): BOOLEAN

Is Current strictly greater than other?

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: NUMBER): BOOLEAN

Is Current greater or equal than other?

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other <= Current)

frozen +: NUMBER

Unary plus of Current.

ensure

  • Result = Current

deferred -: NUMBER

Opposite of Current.

ensure

  • Result /= Void

frozen is_integer_8: BOOLEAN

Does Current value fit on an INTEGER_8?

ensure

  • Result implies is_integer_general_number

frozen is_integer_16: BOOLEAN

Does Current value fit on an INTEGER_16?

ensure

  • Result implies is_integer_general_number

frozen is_integer: BOOLEAN

Does Current value fit on an INTEGER?

ensure

  • Result implies is_integer_general_number

is_integer_32: BOOLEAN

Does Current value fit on an INTEGER?

ensure

  • Result implies is_integer_general_number

frozen is_integer_64: BOOLEAN

Does Current value fit on an INTEGER_64?

ensure

  • Result implies is_integer_general_number

in_range (lower: NUMBER, upper: NUMBER): BOOLEAN

Return True if Current is in range [lower..upper]

ensure

  • Result = (Current >= lower and Current <= upper)

compare (other: NUMBER): INTEGER

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

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

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

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

Is odd ?

require

  • is_integer_general_number

is_even: BOOLEAN

Is even ?

require

  • is_integer_general_number

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

frozen is_integer_general_number: BOOLEAN
frozen is_fraction_general_number: BOOLEAN
frozen fit_real: BOOLEAN
frozen to_integer_8: INTEGER_8

Conversion of Current in an INTEGER_8.

require

  • is_integer_8

frozen to_integer_16: INTEGER_16

Conversion of Current in an INTEGER_16.

require

  • is_integer_16

frozen to_integer: INTEGER

Conversion of Current in an INTEGER.

require

  • is_integer

to_integer_32: INTEGER

Conversion of Current in an INTEGER.

require

  • is_integer

frozen to_integer_64: INTEGER_64

Conversion of Current in an INTEGER.

require

  • is_integer_64

deferred force_to_real_64: REAL

Conversion of Current in a REAL_64.

require

  • fit_real

frozen to_string: STRING

Convert the NUMBER into a new allocated STRING. Note: see also append_in to save memory.

frozen to_unicode_string: UNICODE_STRING

Convert the NUMBER into a new allocated UNICODE_STRING. Note: see also append_in_unicode to save memory.

deferred append_in (buffer: STRING)

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

deferred append_in_unicode (buffer: UNICODE_STRING)

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

frozen 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

frozen 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

frozen 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

frozen 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

frozen to_decimal (digits: INTEGER, all_digits: BOOLEAN): STRING

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

deferred append_decimal_in (buffer: STRING, digits: INTEGER, all_digits: BOOLEAN)

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

frozen decimal_digit: CHARACTER

Gives the corresponding CHARACTER for range 0..9.

require

  • to_integer.in_range(0, 9)

ensure

  • (once "0123456789").has(Result)
  • Current @= Result.value

digit: CHARACTER

Gives the corresponding CHARACTER for range 0..9.

require

  • to_integer.in_range(0, 9)

ensure

  • (once "0123456789").has(Result)
  • Current @= Result.value

divisible (other: NUMBER): BOOLEAN

Is other a valid divisor for Current ?

require

  • other /= Void

one: NUMBER

The neutral element of multiplication.

ensure

  • neutral_element:

    Result is the neutral element of multiplication.

zero: NUMBER

The neutral element of addition.

ensure

  • neutral_element:

    Result is the neutral element of addition.

frozen sign: INTEGER_8

Sign of Current (0 or -1 or 1).

ensure

  • Result = 1 implies is_positive
  • Result = 0 implies is_zero
  • Result = -1 implies is_negative

sqrt: REAL

Compute the square routine.

require

  • fit_real

frozen log: REAL

require

  • fit_real

abs: NUMBER

ensure

  • not Result.is_negative

deferred @+ (other: INTEGER_64): NUMBER

Sum of Current and other.

ensure

  • Result /= Void

@- (other: INTEGER_64): NUMBER

Difference of Current and other.

ensure

  • Result /= Void

deferred @* (other: INTEGER_64): NUMBER

ensure

  • Result /= Void

deferred @/ (other: INTEGER_64): NUMBER

Quotient of Current and other.

require

  • other /= 0

ensure

  • Result /= Void

@^ (exp: INTEGER_64): NUMBER

require

  • is_zero implies exp > 0

ensure

  • Result /= Void

deferred @< (other: INTEGER_64): BOOLEAN

Is Current strictly less than other?

ensure

  • Result = not (Current @>= other)

deferred @<= (other: INTEGER_64): BOOLEAN

Is Current less or equal other?

ensure

  • Result = not (Current @> other)

deferred @> (other: INTEGER_64): BOOLEAN

Is Current strictly greater than other?

ensure

  • Result = not (Current @<= other)

deferred @>= (other: INTEGER_64): BOOLEAN

Is Current greater or equal than other?

ensure

  • Result = not (Current @< other)

deferred #= (other: REAL): BOOLEAN

Is Current equal other?

deferred #< (other: REAL): BOOLEAN

Is Current strictly less than other?

ensure

  • Result implies not (Current #>= other)

deferred #<= (other: REAL): BOOLEAN

Is Current less or equal other?

ensure

  • Result = not (Current #> other)

deferred #> (other: REAL): BOOLEAN

Is Current strictly greater than other?

ensure

  • Result = not (Current #<= other)

deferred #>= (other: REAL): BOOLEAN

Is Current greater or equal than other?

ensure

  • Result = not (Current #< other)

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.

deferred inverse: NUMBER

require

  • divisible(Current)

ensure

  • Result /= Void

deferred numerator: INTEGER_GENERAL_NUMBER
deferred denominator: INTEGER_GENERAL_NUMBER
deferred is_equal (other: FRACTION_GENERAL_NUMBER): 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: FRACTION_GENERAL_NUMBER): 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)

Class invariant