Table of Contents Previous Chapter

5.10 Class DOUBLE

indexing

description: "Real values, double precision"

expanded class interface

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