REAL 64 (interface)

Class Interface

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

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 "/"