Class BOOLEAN

5.6 Class BOOLEAN

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