Table of Contents
Previous Chapter
- indexing
- description: "Real values, single precision"
- expanded class interface
- feature -- Access
- -- Hash code value
- -- (From HASHABLE.)
- good_hash_value: Result >= 0
- -- Neutral element for "*" and "/"
- -- (From NUMERIC.)
- Result_exists: Result /= Void;
- value: Result = 1.0
- -- Sign value (0, ---1 or 1)
- three_way: Result = three_way_comparison (zero)
- -- Neutral element for "+" and "--"
- -- (From NUMERIC.)
- Result_exists: Result /= Void;
- value: Result = 0.0
- feature -- Comparison
- infix "<" (other: like Current): BOOLEAN
- -- Is other greater than current real?
- -- (From COMPARABLE.)
- other_exists: other /= Void
- asymmetric: Result implies not (other < Current)
- infix "<=" (other: like Current): BOOLEAN
- -- Is current object less than or equal to other?
- -- (From COMPARABLE.)
- other_exists: other /= Void
- definition: Result = (Current < other) or is_equal (other);
- infix ">=" (other: like Current): BOOLEAN
- -- Is current object greater than or equal to other?
- -- (From COMPARABLE.)
- other_exists: other /= Void
- definition: Result = (other <= Current)
- infix ">" (other: like Current): BOOLEAN
- -- Is current object greater than other?
- -- (From COMPARABLE.)
- other_exists: other /= Void
- definition: Result = (other < Current)
- max (other: like Current): like Current
- -- The greater of current object and other
- -- (From COMPARABLE.)
- other_exists: other /= Void
- 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.)
- other_exists: other /= Void
- 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.)
- other_exists: other /= Void
- 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.)
- other_exists: other /= Void
- not_exact_zero: Result implies (other /= 0.0)
- exponentiable (other: NUMERIC): BOOLEAN
- -- May current object be elevated to the power other?
- -- (From NUMERIC.)
- other_exists: other /= Void
- safe_values: (other.conforms_to (0) or (other.conforms_to (Current) and (Current >= 0.0))) implies Result
- feature -- Conversion
- -- Smallest integral value no smaller than current object
- result_no_smaller: Result >= Current;
- close_enough: Result -- Current < one
- -- Greatest integral value no greater than current object
- result_no_greater: Result <= Current;
- close_enough: Current -- Result < one
- -- Rounded integral value
- definition: Result = sign * ((abs + 0.5).floor)
- truncated_to_integer: INTEGER
- -- Integer part (same sign, largest absolute
- -- value no greater than current object's)
- feature -- Basic operations
- -- Absolute value
- non_negative: Result >= 0;
- same_absolute_value: (Result = Current) or (Result = --Current)
- infix "*" (other: like Current): like Current
- -- Product by other
- -- (From NUMERIC.)
- other_exists: other /= Void
- result_exists: Result /= Void
- infix "+" (other: like Current): like Current
- -- Sum with other
- -- (From NUMERIC.)
- other_exists: other /= Void
- result_exists: Result /= Void;
- commutative: equal (Result, other + Current)
- infix "--" (other: like Current): like Current
- -- Result of subtracting other
- -- (From NUMERIC.)
- other_exists: other /= Void
- result_exists: Result /= Void
- infix "/" (other: like Current): like Current
- -- Division by other
- -- (From NUMERIC.)
- other_exists: other /= Void;
- good_divisor: divisible (other)
- result_exists: Result /= Void
- infix "^" (other: NUMERIC): DOUBLE
- -- Current real to the power other
- -- (From NUMERIC.)
- other_exists: other /= Void;
- good_exponent: exponentiable (other)
- result_exists: Result /= Void
- -- Unary plus
- -- (From NUMERIC.)
- result_exists: Result /= Void
- prefix "--": like Current
- -- Unary minus
- -- (From NUMERIC.)
- result_exists: Result /= Void
- feature -- Output
- -- Printable representation of real 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
|