5.9 Class REAL PreviousNext

indexing
description: "Real values, simple precision"
expanded class interface
REAL
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 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
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)
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: NUMERIC): DOUBLE
        -- Current real to 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 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

Copyright 1995, Nonprofit International Consortium for Eiffel
mailto:
nice@atlanta.twr.com
Last Updated: 26 October 1997

HomeTocPreviousNext