5.6 Class BOOLEAN PreviousNext

indexing
description: "Truth values, with the boolean operations"
expanded class interface
BOOLEAN
feature -- Access
hash_code: INTEGER
        -- Hash code value
        -- (From HASHABLE.)
    ensure
        good_hash_value: Result >= 0
feature -- Basic operations
infix "and" (other: BOOLEAN): BOOLEAN
        -- Boolean conjunction with other
    require
        other_exists: other /= Void
    ensure
        Result_exists: Result /= Void;
        de_morgan: Result = not (not Current or (not other));
        commutative: Result = (other and Current);
        consistent_with_semi_strict: Result implies (Current and then other)
infix "and then" (other: BOOLEAN): BOOLEAN
        -- Boolean semi-strict conjunction with other
    require
        other_exists: other /= Void
    ensure
        Result_exists: Result /= Void;
        de_morgan: Result = not (not Current or else (not other));
infix "implies" (other: BOOLEAN): BOOLEAN
        -- Boolean implication of other
        -- (semi-strict)
    require
        other_exists: other /= Void
    ensure
        definition: Result = (not Current or else other)
prefix "not": BOOLEAN
        -- Negation.
infix "or" (other: BOOLEAN): BOOLEAN
        -- Boolean disjunction with other
    require
        other_exists: other /= Void
    ensure
        Result_exists: Result /= Void;
        de_morgan: Result = not (not Current and (not other));
        commutative: Result = (other or Current);
        consistent_with_semi_strict: Result implies (Current or else other)
infix "or else" (other: BOOLEAN): BOOLEAN
        -- Boolean semi-strict disjunction with other
    require
        other_exists: other /= Void
    ensure
        Result_exists: Result /= Void;
        de_morgan: Result = not (not Current and then (not other));
infix "xor" (other: BOOLEAN): BOOLEAN
        -- Boolean exclusive or with other
    require
        other_exists: other /= Void
    ensure
        definition: Result = ((Current or other) and not (Current and other))
feature -- Output
out: STRING
        -- Printable representation of boolean
invariant
involutive_negation: is_equal (not (not Current));
non_contradiction: not (Current and (not Current));
completeness: Current or (not Current)
end

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

HomeTocPreviousNext