Table of Contents Previous Chapter

5.6 Class BOOLEAN

indexing

description: "Truth values, with the boolean operations"

expanded class interface

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

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

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

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

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

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