View source for REAL 64 (interface)

You do not have permission to edit this page, for the following reasons:
The action you have requested is limited to users in one of the groups: Autoconfirmed users, emailconfirmed, editors.
You must confirm your email address before editing pages. Please set and validate your email address through your user preferences.
You can view and copy the source of this page:
[[Category:ELKS]]
__TOC__

==Class Interface==

<eiffel>indexing
  description: "Real values, 64 bit precision"

class interface REAL_64

inherit

  NUMERIC

  COMPARABLE

  HASHABLE

feature -- Access

  hash_code: INTEGER
      -- Hash code value
      -- (From HASHABLE.)
    ensure
      good_hash_value: Result >= 0

  sign: INTEGER
      -- Sign value (0, -1 or 1)
    ensure
      three_way: Result = three_way_comparison (zero)

  one: like Current
      -- Neutral element for "*" and "/"
      -- (From NUMERIC.)
    ensure
      Result_exists: Result /= Void;
      value: Result = 1.0

  zero: like Current
      -- Neutral element for "+" and "-"
      -- (From NUMERIC.)
    ensure
      Result_exists: Result /= Void;
      value: Result = 0.0

feature -- Comparison

  infix "<" (other: like Current): BOOLEAN
      -- Is other greater than current real?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      asymmetric: Result implies not (other < Current)

  infix "<=" (other: like Current): BOOLEAN
      -- Is current object less than or equal to other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (Current < other) or is_equal (other);

  infix ">=" (other: like Current): BOOLEAN
      -- Is current object greater than or equal to other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (other <= Current)

  infix ">" (other: like Current): BOOLEAN
      -- Is current object greater than other?
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      definition: Result = (other < Current)

  max (other: like Current): like Current
      -- The greater of current object and other
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      current_if_not_smaller: (Current >= other) implies (Result = Current)
      other_if_smaller: (Current < other) implies (Result = other)

  min (other: like Current): like Current
      -- The smaller of current object and other
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      current_if_not_greater: (Current <= other) implies (Result = Current)
      other_if_greater: (Current > other) implies (Result = other)

  three_way_comparison (other: like Current): INTEGER
      -- If current object equal to other, 0; if smaller,
      -- -1; if greater, 1.
      -- (From COMPARABLE.)
    require
      other_exists: other /= Void
    ensure
      equal_zero: (Result = 0) = is_equal (other);
      smaller: (Result = 1) = Current < other;
      greater_positive: (Result = -1) = Current > other

feature -- Status report

  divisible (other: like Current): BOOLEAN
      -- May current object be divided by other?
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      not_exact_zero: Result implies (other /= 0.0)

  exponentiable (other: NUMERIC): BOOLEAN
      -- May current object be elevated to the power other?
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
       safe_values: (other.conforms_to (0) or 
        (other.conforms_to (Current) and (Current >= 0.0)))
          implies Result

  is_special_case: BOOLEAN
      -- Is current object a special case regarding numeric operations?
      -- (From NUMERIC.)
    ensure then
      nan_and_inf_are_special: Result implies is_nan or is_infinity

  is_nan: BOOLEAN
      -- Is current object not a number (NaN)?
    ensure
      quiet_or_signaling: Result = (is_quiet_nan xor is_signaling_nan)

  is_quiet_nan: BOOLEAN
      -- Is current object a quiet NaN?

  is_signaling_nan: BOOLEAN
      -- Is current object a signaling NaN?

  is_infinity: BOOLEAN
      -- Is current object infinity (INF)?
    ensure
      positive_or_negative: Result = (is_positive_infinity xor is_negative_infinity)

  is_positive_infinity: BOOLEAN
      -- Is current object positive infinity (+INF)?

  is_negative_infinity: BOOLEAN
      -- Is current object negative infinity (-INF)?

  is_in_integer_range: BOOLEAN
      -- Is value of current object in range of minimum to maximum value of an INTEGER?
    ensure
      not_special: Result implies not is_special_case

  is_in_integer_32_range: BOOLEAN
      -- Is value of current object in range of minimum to maximum value of an INTEGER_32?
    ensure
      not_special: Result implies not is_special_case

  is_in_integer_64_range: BOOLEAN
      -- Is value of current object in range of minimum to maximum value of an INTEGER_64?
    ensure
      not_special: Result implies not is_special_case

feature -- Conversion

  ceiling: INTEGER
      -- Smallest integral value no smaller than current object
    ensure
      result_no_smaller: is_in_integer_range implies Result >= Current;
      close_enough: is_in_integer_range implies Result - Current < one

  floor: INTEGER
      -- Greatest integral value no greater than current object
    ensure
      result_no_greater: is_in_integer_range implies Result <= Current;
      close_enough: is_in_integer_range implies Current - Result < one

  rounded: INTEGER
      -- Rounded integral value
    ensure
      definition: is_in_integer_range implies Result = sign * ((abs + 0.5).floor)

  truncated_to_integer: INTEGER
      -- Integer part (same sign, largest absolute
      -- value no greater than current object's)
    ensure
      same_sign: not is_special_case implies Result.sign = sign
      definition: is_in_integer_range implies Result = floor

feature -- Basic operations

  abs: like Current
      -- Absolute value
    ensure
      non_negative: not is_nan implies Result >= 0;
      same_absolute_value: not is_nan implies (Result = Current) or (Result = - Current)

  infix "*" (other: like Current): like Current
      -- Product by other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void

  infix "+" (other: like Current): like Current
      -- Sum with other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void;
      commutative: equal (Result, other + Current)

  infix "-" (other: like Current): like Current
      -- Result of subtracting other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void

  infix "/" (other: like Current): like Current
      -- Division by other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void;
      good_divisor: divisible (other)
    require else
      other_exists: other /= Void
    ensure
      result_exists: Result /= Void
    ensure then
      result_correct: not divisble (other) implies Result.is_special_case

  infix "^" (other: NUMERIC): DOUBLE
      -- Current real to power other
      -- (From NUMERIC.)
    require
      other_exists: other /= Void;
      good_exponent: exponentiable (other)
    ensure
      result_exists: Result /= Void

  prefix "+": like Current
      -- Unary plus
      -- (From NUMERIC.)
    ensure
      result_exists: Result /= Void

  prefix "-": like Current
      -- Unary minus
      -- (From NUMERIC.)
    ensure
      result_exists: Result /= Void

feature -- Output

  out: STRING
      -- Printable representation of real value
      -- (From GENERAL.)

invariant

  sign_times_abs: equal (sign * abs, Current)

    -- From COMPARABLE
  irreflexive_comparison: not (Current < Current);

    -- From NUMERIC
  neutral_addition: not is_special_case implies equal (Current + zero, Current);
  self_subtraction: not is_special_case implies equal (Current - Current, zero);
  neutral_multiplication: not is_special_case implies equal (Current * one, Current);
  self_division: divisible not is_special_case implies (Current) implies equal (Current / Current, one)

end
</eiffel>

==Changes to ELKS 95==

new features:
* is_nan
* is_infinity
* is_positive_infinity
* is_negative_infinity
* is_in_integer_range
* is_in_integer_32_range
* is_in_integer_64_range

changed feature contracts:
* ceiling
* floor
* rounded
* truncated_to_integer
* abs
* infix "/"
Return to REAL 64 (interface).
Retrieved from "https://dev.eiffel.com/REAL_64_(interface)"
View source for REAL 64 (interface)

Navigation

Development

Wiki

Search

Tools
