EiffelBase class
(HTML page generated by ISE Eiffel 4.2)

indexing
	description: "References to objects containing a boolean value";
	status: "See notice at end of class";
	date: "$Date: 2007-03-30 11:10:11 -0800 (Fri, 30 Mar 2007) $";
	revision: "$Revision: 95354 $"

class BOOLEAN_REF

inherit
	HASHABLE
		redefine
			is_hashable, out
		end

feature -- Access

	item: BOOLEAN;
			-- Boolean value

	hash_code: INTEGER is
			-- Hash code value
		do
			Result := 1
		end;

feature -- Status report

	is_hashable: BOOLEAN is
			-- May current object be hashed?
			-- (True if it is not its type's default.)
		do
			Result := item
		end;

feature -- Element change

	set_item (b: BOOLEAN) is
			-- Make b the item value.
		do
			item := b
		end;

feature -- Basic operations

	infix "and" (other: like Current): BOOLEAN is
			-- Boolean conjunction with other
		require
			other_exists: other /= void
		do
			Result := item and other.item
		ensure
			result_exists: Result /= void;
			de_morgan: Result = not(notCurrent or notother);
			commutative: Result = (other and Current);
			consistent_with_semi_strict: Result implies (Current and then other)
		end;

	infix "and then" (other: like Current): BOOLEAN is
			-- Boolean semi-strict conjunction with other
		require
			other_exists: other /= void
		do
			Result := item and then other.item
		ensure
			result_exists: Result /= void;
			de_morgan: Result = not(notCurrent or else notother)
		end;

	infix "implies" (other: like Current): BOOLEAN is
			-- Boolean implication of other
			-- (semi-strict)
		require
			other_exists: other /= void
		do
			Result := item implies other.item
		ensure
			definition: Result = (notCurrent or else other)
		end;

	prefix "not": like Current is
			-- Negation
		do
			create Result;
			Result.set_item (notitem)
		end;

	infix "or" (other: like Current): BOOLEAN is
			-- Boolean disjunction with other
		require
			other_exists: other /= void
		do
			Result := item or other.item
		ensure
			result_exists: Result /= void;
			de_morgan: Result = not(notCurrent and notother);
			commutative: Result = (other or Current);
			consistent_with_semi_strict: Result implies (Current or else other)
		end;

	infix "or else" (other: like Current): BOOLEAN is
			-- Boolean semi-strict disjunction with other
		require
			other_exists: other /= void
		do
			Result := item or else other.item
		ensure
			result_exists: Result /= void;
			de_morgan: Result = not(notCurrent and then notother)
		end;

	infix "xor" (other: like Current): BOOLEAN is
			-- Boolean exclusive or with other
		require
			other_exists: other /= void
		do
			Result := item xor other.item
		ensure
			definition: Result = ((Current or other) and not(Current and other))
		end;

feature -- Output

	out: STRING is
			-- Printable representation of boolean
		do
			Result := c_outb (item)
		end;

feature {NONE} -- Implementation

	c_outb (b: BOOLEAN): STRING is
			-- Printable representation of boolean
		external
			"C | %"eif_out.h%""
		end;

invariant

	involutive_negation: is_equal (not(notCurrent));
	non_contradiction: not(Current and (notCurrent));
	completeness: Current or else (notCurrent);

end -- class BOOLEAN_REF

© 1985-2012 Eiffel Software. All rights reserved. -- Privacy Policy