This site contains older material on Eiffel. For the main Eiffel page, see http://www.eiffel.com.

Table of Contents Previous Chapter

5.10 Class DOUBLE

indexing
    description: "Real values, double precision"
expanded class interface
    DOUBLE
feature -- Access
    hash_code: INTEGER
-- Hash code value
-- (From HASHABLE.)
      ensure
good_hash_value: Result >= 0
    one: like Current
-- Neutral element for "*" and "/"
-- (From NUMERIC.)
      ensure
Result_exists: Result /= Void;
value: Result = 1.0
    sign: INTEGER
-- Sign value (0, ---1 or 1)
      ensure
three_way: Result = three_way_comparison (zero)
    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 double?
-- (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.
      require
other_exists: other /= Void
-- (From COMPARABLE.)
      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
feature -- Conversion
    ceiling: INTEGER
-- Smallest integral value no smaller than current object
      ensure
result_no_smaller: Result >= Current;
close_enough: Result -- Current < one
    floor: INTEGER
-- Greatest integral value no greater than current object
      ensure
result_no_greater: Result <= Current;
close_enough: Current -- Result < one
    rounded: INTEGER
-- Rounded integral value
      ensure
definition: Result = sign * ((abs + 0.5).floor)
    truncated_to_integer: INTEGER
-- Integer part (same sign, largest absolute
-- value no greater than current object's)
    truncated_to_real: REAL
-- Real part (same sign, largest absolute
-- value no greater than current object's)
feature -- Basic operations
    abs: like Current
-- Absolute value
      ensure
non_negative: Result >= 0;
same_absolute_value: (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)
      ensure
result_exists: Result /= Void
    infix "^" (other: like Current): like Current
-- Current double to the 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 double value
-- (From GENERAL.)
invariant
    irreflexive_comparison: not (Current < Current);
    neutral_addition: equal (Current + zero, Current);
    self_subtraction: equal (Current -- Current, zero);
    neutral_multiplication: equal (Current * one, Current);
    self_division: divisible (Current) implies equal (Current / Current, one)
    sign_times_abs: equal (sign*abs, Current)
end

Table of Contents Next Chapter