indexing
	description: "Sets whose items may be compared according to a total order relation"
	status: "See notice at end of class"
	names: comparable_set, comparable_struct
	access: membership, min, max
	contents: generic
	date: "$Date$"
	revision: "$Revision$"
deferred class interface
	COMPARABLE_SET [G -> COMPARABLE]
feature 
	has (v: like item): BOOLEAN
			v
			
			object_comparison
			 LINEAR
		ensure  CONTAINER
			not_found_in_empty: Result implies not is_empty
feature 
	count: INTEGER
			
			 SET
	max: G
			
		require
			not_empty: not is_empty
	min: G
			
		require
			not_empty: not is_empty
feature 
	disjoint (other: SUBSET [G]): BOOLEAN
			other
			
			
			
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
	is_subset (other: SUBSET [G]): BOOLEAN
			other
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
	is_superset (other: SUBSET [G]): BOOLEAN
			other
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
feature 
	extendible: BOOLEAN
			
			 COLLECTION
	is_empty: BOOLEAN
			
			 CONTAINER
	is_inserted (v: G): BOOLEAN
			v
			
			
			
			 COLLECTION
	object_comparison: BOOLEAN
			equal=
			=
			 CONTAINER
	prunable: BOOLEAN
			
			 COLLECTION
feature 
	compare_objects
			equal
			=
			 CONTAINER
		require  CONTAINER
			changeable_comparison_criterion
		ensure  CONTAINER
			object_comparison
	compare_references
			=
			equal
			 CONTAINER
		require  CONTAINER
			changeable_comparison_criterion
		ensure  CONTAINER
			reference_comparison: not object_comparison
feature 
	extend (v: G)
			v
			SETput
			 SET
		require  COLLECTION
			extendible: extendible
		ensure  COLLECTION
			item_inserted: is_inserted (v)
		ensure then  SET
			in_set_already: old has (v) implies (count = old count)
			added_to_set: not old has (v) implies (count = old count + 1)
	fill (other: CONTAINER [G])
			other
			other
			
			 COLLECTION
		require  COLLECTION
			other_not_void: other /= void
			extendible
	merge (other: CONTAINER [G])
			other
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
	put (v: G)
			v
			SETextend
			 SET
		require  COLLECTION
			extendible: extendible
		ensure  COLLECTION
			item_inserted: is_inserted (v)
		ensure then  SET
			in_set_already: old has (v) implies (count = old count)
			added_to_set: not old has (v) implies (count = old count + 1)
feature 
	changeable_comparison_criterion: BOOLEAN
			object_comparison
			
			
			 SET
		ensure then  SET
			only_on_empty: Result = is_empty
	prune (v: G)
			v
			 SET
		require  COLLECTION
			prunable: prunable
		ensure then  SET
			removed_count_change: old has (v) implies (count = old count - 1)
			not_removed_no_count_change: not old has (v) implies (count = old count)
			item_deleted: not has (v)
	prune_all (v: G)
			v
			
			object_comparison
			 COLLECTION
		require  COLLECTION
			prunable
		ensure  COLLECTION
			no_more_occurrences: not has (v)
	wipe_out
			
			 COLLECTION
		require  COLLECTION
			prunable
		ensure  COLLECTION
			wiped_out: is_empty
feature 
	linear_representation: LINEAR [G]
			
			 LINEAR
feature 
	duplicate (n: INTEGER): like Current
			ncount
			
			 SUBSET
		require  SUBSET
			non_negative: n >= 0
		ensure  SUBSET
			correct_count_1: n <= count implies Result.count = n
			correct_count_2: n >= count implies Result.count = count
feature 
	intersect (other: SUBSET [G])
			other
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
		ensure  SUBSET
			is_subset_other: is_subset (other)
	subtract (other: SUBSET [G])
			other
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
		ensure  SUBSET
			is_disjoint: disjoint (other)
	symdif (other: SUBSET [G])
			other
			other
			
			
			
			 SUBSET
		require  SUBSET
			set_exists: other /= void
			same_rule: object_comparison = other.object_comparison
invariant
		 ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		 COMPARABLE_STRUCT
	empty_constraint: min_max_available implies not is_empty
		 BILINEAR
	not_both: not (after and before)
	before_constraint: before implies off
		 LINEAR
	after_constraint: after implies off
		 TRAVERSABLE
	empty_constraint: is_empty implies off
indexing
	library: "[
			EiffelBase: Library of reusable components for Eiffel.
	]"
	status: "[
			Copyright 1986-2001 Interactive Software Engineering (ISE).
			For ISE customers the original versions are an ISE product
			covered by the ISE Eiffel license and support agreements.
	]"
	license: "[
			EiffelBase may now be used by anyone as FREE SOFTWARE to
			develop any product, public-domain or commercial, without
			payment to ISE, under the terms of the ISE Free Eiffel Library
			License (IFELL) at http://eiffel.com/products/base/license.html.
	]"
	source: "[
			Interactive Software Engineering Inc.
			ISE Building
			360 Storke Road, Goleta, CA 93117 USA
			Telephone 805-685-1006, Fax 805-685-6869
			Electronic mail <info@eiffel.com>
			Customer support http://support.eiffel.com
	]"
	info: "[
			For latest info see award-winning pages: http://eiffel.com
	]"
end -- COMPARABLE_SET