REAL 64 (interface)

class REAL_64
 
inherit
 
  NUMERIC
 
  HASHABLE
 
  COMPARABLE
 
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
 
  is_nan: BOOLEAN
      -- Is current object not a number (NaN)?
 
  is_infinity: BOOLEAN
      -- Is current object infinity (INF)?
 
  is_positive_infinity: BOOLEAN
      -- Is current object positive infinity (+INF)?
 
  is_negative_infinity: BOOLEAN
      -- Is current object negative infinity (-INF)?
 
  is_in_integer_32_range: BOOLEAN
      -- Is value of current object in range of minimum to maximum value of an INTEGER_32?
 
  is_in_integer_64_range: BOOLEAN
      -- Is value of current object in range of minimum to maximum value of an INTEGER_64?
 
end