indexing
	description: "Structures that can be traversed and modified through integer access"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

deferred class interface
	DS_INDEXABLE [G]

feature -- Access

	first: G
			-- First item in structure
		require -- from DS_EXTENDIBLE
			not_empty: not is_empty
		ensure then
			definition: Result = item (1)

	item (k: INTEGER): G
			-- Item associated with k
			-- Was declared in DS_TABLE as synonym of @ and item.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)

	last: G
			-- Last item in structure
		require
			not_empty: not is_empty
		ensure
			definition: Result = item (count)

	infix "@" (k: INTEGER): G
			-- Item associated with k
			-- Was declared in DS_TABLE as synonym of @ and item.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)
	
feature -- Measurement

	count: INTEGER
			-- Number of items in structure
			-- (from DS_CONTAINER)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is current structure equal to other?
			-- (from DS_CONTAINER)
		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 -- from DS_CONTAINER
			same_count: Result implies count = other.count
		ensure then -- from DS_CONTAINER
			same_count: Result implies count = other.count
	
feature -- Status report

	extendible (n: INTEGER): BOOLEAN
			-- May structure be extended with n items?
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			positive_n: n >= 0

	is_empty: BOOLEAN
			-- Is structure empty?
			-- (from DS_CONTAINER)

	sorted (sorter: DS_SORTER [G]): BOOLEAN
			-- Is structure sorted according to sorter's criterion?
			-- (from DS_SORTABLE)
		require -- from DS_SORTABLE
			sorter_not_void: sorter /= void

	valid_entry (i: INTEGER): BOOLEAN
			-- Is there an item at index i?
		ensure -- from DS_TABLE
			valid_key: Result implies valid_index (k)
		ensure then
			definition: Result = (1 <= i and i <= count)

	valid_index (i: INTEGER): BOOLEAN
			-- Is i a valid index?
		ensure then
			definition: Result = (1 <= i and i <= count + 1)
	
feature -- Element change

	append_first (other: DS_LINEAR [G])
			-- Add items of other to structure.
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			other_not_void: other /= void
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count + other.count

	append (other: DS_LINEAR [G]; i: INTEGER)
			-- Add items of other at i-th position.
		require
			other_not_void: other /= void;
			valid_index: valid_index (i)
		ensure
			new_count: count = old count + other.count

	append_last (other: DS_LINEAR [G])
			-- Add items of other to end of structure.
		require
			other_not_void: other /= void
		ensure
			new_count: count = old count + other.count

	extend (other: DS_LINEAR [G]; i: INTEGER)
			-- Add items of other at i-th position.
		require
			other_not_void: other /= void;
			extendible: extendible (other.count);
			valid_index: valid_index (i)
		ensure
			new_count: count = old count + other.count

	extend_first (other: DS_LINEAR [G])
			-- Add items of other to structure.
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			other_not_void: other /= void;
			extendible: extendible (other.count)
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count + other.count

	extend_last (other: DS_LINEAR [G])
			-- Add items of other to end of structure.
		require
			other_not_void: other /= void;
			extendible: extendible (other.count)
		ensure
			new_count: count = old count + other.count

	force (v: G; i: INTEGER)
			-- Add v at i-th position.
		require -- from DS_TABLE
			valid_key: valid_index (k)
		ensure -- from DS_TABLE
			valid_entry: valid_entry (k);
			inserted: item (k) = v
		ensure then
			one_more: count = old count + 1

	force_first (v: G)
			-- Add v to beginning of structure.
		ensure -- from DS_EXTENDIBLE
			one_more: count = old count + 1
		ensure then
			inserted: first = v

	force_last (v: G)
			-- Add v to end of structure.
		ensure
			one_more: count = old count + 1;
			inserted: last = v

	put (v: G; i: INTEGER)
			-- Add v at i-th position.
		require
			extendible: extendible (1);
			valid_index: valid_index (i)
		ensure
			one_more: count = old count + 1;
			valid_entry: valid_entry (i);
			inserted: item (i) = v

	put_first (v: G)
			-- Add v to beginning of structure.
		require -- from DS_EXTENDIBLE
			extendible: extendible (1)
		ensure -- from DS_EXTENDIBLE
			one_more: count = old count + 1
		ensure then
			inserted: first = v

	put_last (v: G)
			-- Add v to end of structure.
		require
			extendible: extendible (1)
		ensure
			one_more: count = old count + 1;
			inserted: last = v

	replace (v: G; k: INTEGER)
			-- Replace item associated with k by v.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)
		ensure -- from DS_TABLE
			replaced: item (k) = v;
			same_count: count = old count
	
feature -- Removal

	keep_first (n: INTEGER)
			-- Keep n items in structure.
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_EXTENDIBLE
			new_count: count = n

	keep_last (n: INTEGER)
			-- Keep n last items in structure.
		require
			valid_n: 0 <= n and n <= count
		ensure
			new_count: count = n

	prune (n: INTEGER; i: INTEGER)
			-- Remove n items at and after i-th position.
		require
			valid_entry: valid_entry (i);
			valid_n: 0 <= n and n <= count - i + 1
		ensure
			new_count: count = old count - n

	prune_first (n: INTEGER)
			-- Remove n items from structure.
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count - n

	prune_last (n: INTEGER)
			-- Remove n last items from structure.
		require
			valid_n: 0 <= n and n <= count
		ensure
			new_count: count = old count - n

	remove_first
			-- Remove an item from structure.
			-- (from DS_EXTENDIBLE)
		require -- from DS_EXTENDIBLE
			not_empty: not is_empty
		ensure -- from DS_EXTENDIBLE
			one_less: count = old count - 1

	remove (k: INTEGER)
			-- Remove item associated with k.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)
		ensure -- from DS_TABLE
			one_less: count = old count - 1

	remove_last
			-- Remove last item from structure.
		require
			not_empty: not is_empty
		ensure
			one_less: count = old count - 1

	wipe_out
			-- Remove all items from structure.
			-- (from DS_CONTAINER)
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
	
feature -- Transformation

	swap (k, l: INTEGER)
			-- Exchange items associated with k and l.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_k: valid_entry (k);
			valid_l: valid_entry (l)
		ensure -- from DS_TABLE
			same_count: count = old count;
			new_k: item (k) = old item (l);
			new_l: item (l) = old item (k)
	
feature -- Sort

	sort (sorter: DS_SORTER [G])
			-- Sort structure using sorter's algorithm.
			-- (from DS_SORTABLE)
		require -- from DS_SORTABLE
			sorter_not_void: sorter /= void
		ensure -- from DS_SORTABLE
			sorted: sorted (sorter)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: is_empty = (count = 0);

end -- class DS_INDEXABLE