indexing
description: "References to objects containing a double-precision real number"
class interface
DOUBLE_REF
feature -- Access
hash_code: INTEGER
-- Hash code value
ensure -- from HASHABLE
good_hash_value: Result >= 0
item: DOUBLE
-- Numeric double value
one: DOUBLE
-- Neutral element for "*" and "/"
ensure
value: Result = 1.0
sign: INTEGER
-- Sign value (0, -1 or 1)
ensure
three_way: Result = three_way_comparison (zero)
zero: DOUBLE
-- Neutral element for "+" and "-"
ensure
value: Result = 0.0
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object of the same type
-- as current object and identical to it?
require -- COMPARABLE
precursor: True
require -- from GENERAL
other_not_void: other /= void
ensure then -- from COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
max (other: DOUBLE_REF): DOUBLE
-- The greater of current object and other
require
other_exists: other /= void
min (other: DOUBLE_REF): DOUBLE
-- The smaller of current object and other
require
other_exists: other /= void
three_way_comparison (other: DOUBLE_REF): INTEGER
-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
equal_zero: (Result = 0) = is_equal (other);
smaller_negative: (Result = - 1) = (Current < other);
greater_positive: (Result = 1) = (Current > other)
infix "<" (other: like Current): BOOLEAN
-- Is other greater than current double?
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = ((Current < other) or is_equal (other))
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other <= Current)
feature -- Status report
divisible (other: DOUBLE_REF): BOOLEAN
-- May current object be divided by other?
require -- from NUMERIC
other_exists: other /= void
ensure then
not_exact_zero: Result implies (other.item /= 0.0)
exponentiable (other: NUMERIC): BOOLEAN
-- May current object be elevated to the power other?
require -- from NUMERIC
other_exists: other /= void
ensure then
safe_values: ((other.conforms_to (0) and item /= 0.0) or (other.conforms_to (0.0) and item > 0.0)) implies Result
is_hashable: BOOLEAN
-- May current object be hashed?
-- (True if it is not its type's default.)
ensure -- from HASHABLE
ok_if_not_default: Result implies (Current /= default)
feature -- Element change
set_item (d: DOUBLE)
-- Make d the item value.
feature -- Conversion
ceiling: INTEGER
-- Smallest integral value no smaller than current object
ensure
result_no_smaller: Result >= item;
close_enough: Result - item < one
floor: INTEGER
-- Greatest integral value no greater than current object
ensure
result_no_greater: Result <= item;
close_enough: item - 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: DOUBLE
-- Absolute value
ensure
non_negative: Result >= 0.0;
same_absolute_value: (Result = item) or (Result = - item)
infix "*" (other: like Current): like Current
-- Product with other
require -- from NUMERIC
other_exists: other /= void
ensure -- from NUMERIC
result_exists: Result /= void
prefix "+ ": like Current
-- Unary plus
ensure -- from NUMERIC
result_exists: Result /= void
infix "+" (other: like Current): like Current
-- Sum with other
require -- from NUMERIC
other_exists: other /= void
ensure -- from NUMERIC
result_exists: Result /= void;
commutative: equal (Result, other + Current)
prefix "- ": like Current
-- Unary minus
ensure -- from NUMERIC
result_exists: Result /= void
infix "-" (other: like Current): like Current
-- Result of subtracting other
require -- from NUMERIC
other_exists: other /= void
ensure -- from NUMERIC
result_exists: Result /= void
infix "/" (other: like Current): like Current
-- Division by other
require -- from NUMERIC
other_exists: other /= void;
good_divisor: divisible (other)
ensure -- from NUMERIC
result_exists: Result /= void
infix "^" (other: NUMERIC): DOUBLE_REF
-- Current double to the power other
require -- from NUMERIC
other_exists: other /= void;
good_exponent: exponentiable (other)
ensure -- from NUMERIC
result_exists: Result /= void
feature -- Output
out: STRING
-- Printable representation of double value
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
sign_times_abs: sign * abs = item;
-- from COMPARABLE
irreflexive_comparison: not (Current < Current);
end -- class DOUBLE_REF