indexing
	description: "Objects that may be compared according to a total order relation"
	note: "The basic operation is `<%' (less than); others are defined in terms of this operation and `is_equal%'."
	names: comparable, comparison

deferred class interface
	COMPARABLE

feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is other attached to an object of the same type
			-- as current object and identical to it?
		require -- from GENERAL
			other_not_void: other /= void
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
		ensure then
			trichotomy: Result = (not (Current < other) and not (other < Current))

	max (other: like Current): like Current
			-- The greater of current object and other
		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
		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
		require
			other_exists: other /= void
		ensure
			equal_zero: (Result = 0) = is_equal (other);
			smaller_negative: (Result = - 1) = (Current < other);
			greater_positive: (Result = 1) = (Current > other)

	infix "<" (other: like Current): BOOLEAN
			-- Is current object less than other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then
			asymmetric: Result implies not (other < Current)

	infix "<=" (other: like Current): BOOLEAN
			-- Is current object less than or equal to other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then
			definition: Result = ((Current < other) or is_equal (other))

	infix ">" (other: like Current): BOOLEAN
			-- Is current object greater than other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then
			definition: Result = (other < Current)

	infix ">=" (other: like Current): BOOLEAN
			-- Is current object greater than or equal to other?
		require -- from PART_COMPARABLE
			other_exists: other /= void
		ensure then
			definition: Result = (other <= Current)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	irreflexive_comparison: not (Current < Current);

end -- class COMPARABLE