indexing
	description: "Sets of integers with a finite number of items"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

class interface
	FIXED_INTEGER_SET

create 

	make (n: INTEGER)
			-- Make set for at most n integers from 1 to n.
		require
			n_positive: n > 0
		ensure
			set_empty: is_empty

feature -- Initialization

	make (n: INTEGER)
			-- Make set for at most n integers from 1 to n.
		require
			n_positive: n > 0
		ensure
			set_empty: is_empty

	boolean_set_make (n: INTEGER)
			-- Allocate area of n booleans.
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			non_negative_size: n >= 0
		ensure -- from BOOL_STRING
			correct_allocation: count = n
	
feature -- Access

	has (i: INTEGER): BOOLEAN
			-- Is i in set?
		require
			index_large_enough: 1 <= i
			index_small_enough: i <= count

	is_empty: BOOLEAN
			-- Is current set empty?

	item (i: INTEGER): BOOLEAN
			-- Boolean at i-th position,
			-- beginning at left, 1 origin
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			index_large_enough: 1 <= i
			index_small_enough: i <= count

	largest: INTEGER
			-- Largest integer in set;
			-- 0 if set empty

	next (p: INTEGER): INTEGER
			-- Next integer in set following p;
			-- count + 1 if p equals largest
		require
			p_in_set: p >= 1 and p <= count

	smallest: INTEGER
			-- Smallest integer in set;
			-- count + 1 if set empty
	
feature -- Measurement

	count: INTEGER
			-- Number of boolean in the area.
			-- (from BOOL_STRING)
	
feature -- Element change

	all_false
			-- Set all booleans to false.
			-- (from BOOL_STRING)

	all_true
			-- Set all booleans to true.
			-- (from BOOL_STRING)

	put (i: INTEGER)
			-- Insert i into set.
		require
			index_large_enough: 1 <= i
			index_small_enough: i <= count
		ensure
			is_in_set: has (i)

	bool_string_put (v: like item; i: INTEGER)
			-- Put boolean v at i-th position
			-- beginning at left, 1 origin.
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			index_large_enough: 1 <= i
			index_small_enough: i <= count
	
feature -- Removal

	remove (i: INTEGER)
			-- Delete i from set.
		require
			index_large_enough: 1 <= i
			index_small_enough: i <= count
		ensure
			is_not_in_set: not has (i)
	
feature -- Conversion

	to_c: ANY
	
feature -- Basic operations

	left_shifted (n: INTEGER): like Current
			-- Left shifted 'Current' set, by n positions
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			non_negative_shift: n >= 0

	right_shifted (n: INTEGER): like Current
			-- Right shifted 'Current' set, by n positions
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			non_negative_shift: n >= 0

	infix "and" (other: like Current): like Current
			-- Logical and of 'Current' and other
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			other_not_void: other /= void
			same_size: other.count = count

	prefix "not": like Current
			-- Negation of 'Current'
			-- (from BOOL_STRING)

	infix "or" (other: like Current): like Current
			-- Logical or of 'Current' and other
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			other_not_void: other /= void
			same_size: other.count = count

	infix "xor" (other: like Current): like Current
			-- Logical exclusive or of 'Current' and other
			-- (from BOOL_STRING)
		require -- from BOOL_STRING
			other_not_void: other /= void
			same_size: other.count = count
	
feature -- Output

	print
			-- List all items in set.
	
invariant

	positive_size: count > 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class FIXED_INTEGER_SET