indexing
	description: "Adapter for linked lists"
	author: "Patrick Schoenbach"

deferred class interface
	LIST_ADAPTER [G]

feature -- Access

	first: G
			-- First item in structure
			-- (from DS_INDEXABLE)
		require -- from DS_LINEAR
			not_empty: not empty
		require -- from DS_EXTENDIBLE
			not_empty: not empty
		ensure -- from DS_LINEAR
			has_first: has (Result)
		ensure then -- from DS_INDEXABLE
			definition: Result = i_th (1)
		ensure then -- from DS_INDEXABLE
			definition: Result = i_th (1)

	index: INTEGER
			-- Current index

	item: G
			-- Current item
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off

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

	last: G
			-- Last item in structure
			-- (from DS_INDEXABLE)
		require -- from DS_BILINEAR
			not_empty: not empty
		require -- from DS_INDEXABLE
			not_empty: not empty
		require -- from DS_INDEXABLE
			not_empty: not empty
		ensure -- from DS_BILINEAR
			has_last: has (Result)
		ensure -- from DS_INDEXABLE
			definition: Result = i_th (count)
		ensure -- from DS_INDEXABLE
			definition: Result = i_th (count)

	new_cursor: DS_BILINEAR_CURSOR [G]
			-- New cursor for traversal
			-- (from DS_BILINEAR)
		ensure -- from DS_TRAVERSABLE
			cursor_not_void: Result /= void;
			valid_cursor: valid_cursor (Result)

	list_searcher: DS_BILINEAR_SEARCHER [G]
			-- Structure searcher
			-- (from DS_BILINEAR)

	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

	capacity: INTEGER
			-- Capacity of list

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

	occurrences (v: G): INTEGER
			-- Number of times v appears in structure
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			positive: Result >= 0;
			has: has (v) implies Result >= 1
	
feature -- Status report

	after: BOOLEAN
			-- Is there no valid item to the left of cursor?

	before: BOOLEAN
			-- Is there no valid item to the right of cursor?

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

	Full: BOOLEAN is false
			-- Is container full? (Answer: no)

	has (v: G): BOOLEAN
			-- Does structure incluse v?
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			not_empty: Result implies not empty

	Insertable: BOOLEAN is true
			-- Can items be inserted in the middle of container? (Answer: yes)

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

	isfirst: BOOLEAN
			-- Is cursor on first item?

	islast: BOOLEAN
			-- Is cursor on last item?

	off: BOOLEAN
			-- Is cursor off the list?

	Prunable: BOOLEAN is true
			-- Can items be removed from container? (Answer: yes)

	Resizable: BOOLEAN is false
			-- Can container be resized? (Answer: no)

	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_cursor (a_cursor: like new_cursor): BOOLEAN
			-- Is a_cursor a valid cursor?
			-- (A cursor might become invalid if structure
			-- has been modified during traversal.)
			-- (from DS_TRAVERSABLE)
		require -- from DS_TRAVERSABLE
			a_cursor_not_void: a_cursor /= void
		ensure -- from DS_TRAVERSABLE
			is_valid: Result implies a_cursor.is_valid

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

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

	finish
			-- Move cursor to last item.

	forth
			-- Move cursor forwards.
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after
		ensure then -- from LINEAR_CONTAINER
			next_position: index = old index + 1

	go_i_th (i: INTEGER)
			-- Move cursor to i-th item.
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)
		ensure -- from SEQUENCIAL_CONTAINER
			i_th_position: index = i

	start
			-- Move cursor to first item.
		require -- from SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from SEQUENCIAL_CONTAINER
			cursor_at_start: isfirst
	
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
		require -- from DS_EXTENDIBLE
			other_not_void: other /= void
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count + other.count
		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.
			-- (from DS_INDEXABLE)
		require -- from DS_INDEXABLE
			other_not_void: other /= void;
			valid_index: valid_index (i)
		ensure -- from DS_INDEXABLE
			new_count: count = old count + other.count

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

	append_left (other: DS_LINEAR [G]; a_cursor: like new_cursor)
			-- Add items of other to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			other_not_void: other /= void;
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.before
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count

	append_right (other: DS_LINEAR [G]; a_cursor: like new_cursor)
			-- Add items of other to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			other_not_void: other /= void;
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_after: not a_cursor.after
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count

	extend (v: G)
			-- Add v to end of container.
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		ensure then -- from LINEAR_CONTAINER
			extended: i_th (count) = v;
			count_increased: count = old count + 1;
			index_unchanged: not old empty implies index = old index

	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)
		require -- from DS_EXTENDIBLE
			other_not_void: other /= void;
			extendible: extendible (other.count)
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count + other.count
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count + other.count

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

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

	extend_left (other: DS_LINEAR [G]; a_cursor: like new_cursor)
			-- Add items of other to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			other_not_void: other /= void;
			extendible: extendible (other.count);
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.before
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count

	extend_right (other: DS_LINEAR [G]; a_cursor: like new_cursor)
			-- Add items of other to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			other_not_void: other /= void;
			extendible: extendible (other.count);
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_after: not a_cursor.after
		ensure -- from DS_DYNAMIC
			new_count: count = old count + other.count

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

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

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

	force_left (v: G; a_cursor: like new_cursor)
			-- Add v to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.before
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1

	force_right (v: G; a_cursor: like new_cursor)
			-- Add v to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_after: not a_cursor.after
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1

	put (v: G)
			-- Replace current item with v.
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then -- from LINEAR_CONTAINER
			replaced: item = v;
			count_unchanged: count = old count;
			index_unchanged: index = old index

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

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

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

	put_left (v: G)
			-- Insert v to the left of current position.
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_before: not before
		ensure then -- from LINEAR_CONTAINER
			inserted: i_th (index - 1) = v;
			count_increased: count = old count + 1;
			index_increased: index = old index + 1

	list_put_left (v: G; a_cursor: like new_cursor)
			-- Add v to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			extendible: extendible (1);
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.before
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1

	put_right (v: G)
			-- Insert v to the right of current position.
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_after: not after
		ensure then -- from LINEAR_CONTAINER
			inserted: i_th (index + 1) = v;
			count_increased: count = old count + 1;
			index_unchanged: index = old index

	list_put_right (v: G; a_cursor: like new_cursor)
			-- Add v to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			extendible: extendible (1);
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_after: not a_cursor.after
		ensure -- from DS_DYNAMIC
			one_more: count = old count + 1

	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: i_th (k) = v;
			same_count: count = old count
	
feature -- Removal

	delete (v: G)
			-- Remove all occurrences of v.
			-- (Use searcher's comparison criterion.)
			-- (from DS_DYNAMIC)
		ensure -- from DS_DYNAMIC
			deleted: not has (v)

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

	keep_last (n: INTEGER)
			-- Keep n last items in structure.
			-- (from DS_INDEXABLE)
		require -- from DS_DYNAMIC
			valid_n: 0 <= n and n <= count
		require -- from DS_INDEXABLE
			valid_n: 0 <= n and n <= count
		require -- from DS_INDEXABLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_DYNAMIC
			new_count: count = n
		ensure -- from DS_INDEXABLE
			new_count: count = n
		ensure -- from DS_INDEXABLE
			new_count: 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
		require -- from DS_EXTENDIBLE
			valid_n: 0 <= n and n <= count
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count - n
		ensure -- from DS_EXTENDIBLE
			new_count: count = old count - n

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

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

	prune_left (n: INTEGER; a_cursor: like new_cursor)
			-- Remove n items to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			valid_n: 0 <= n and n < a_cursor.index
		ensure -- from DS_DYNAMIC
			new_count: count = old count - n

	prune_right (n: INTEGER; a_cursor: like new_cursor)
			-- Remove n items to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			valid_n: 0 <= n and n <= count - a_cursor.index
		ensure -- from DS_DYNAMIC
			new_count: count = old count - n

	remove
			-- Remove current item.
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then -- from LINEAR_CONTAINER
			count_decreased: count = old count - 1;
			index_unchanged: not off implies index = old index

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

	list_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_at (a_cursor: like new_cursor)
			-- Remove item at a_cursor position.
			-- Move a_cursor to next position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_off: not a_cursor.off
		ensure -- from DS_DYNAMIC
			one_less: count = old count - 1

	remove_last
			-- Remove last item from structure.
			-- (from DS_INDEXABLE)
		require -- from DS_DYNAMIC
			not_empty: not empty
		require -- from DS_INDEXABLE
			not_empty: not empty
		require -- from DS_INDEXABLE
			not_empty: not empty
		ensure -- from DS_DYNAMIC
			one_less: count = old count - 1
		ensure -- from DS_INDEXABLE
			one_less: count = old count - 1
		ensure -- from DS_INDEXABLE
			one_less: count = old count - 1

	remove_left (a_cursor: like new_cursor)
			-- Remove item to left of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			not_empty: not empty;
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.before;
			not_first: not a_cursor.is_first
		ensure -- from DS_DYNAMIC
			one_less: count = old count - 1

	remove_right (a_cursor: like new_cursor)
			-- Remove item to right of a_cursor position.
			-- (from DS_DYNAMIC)
		require -- from DS_DYNAMIC
			not_empty: not empty;
			cursor_not_void: a_cursor /= void;
			valid_cursor: valid_cursor (a_cursor);
			not_before: not a_cursor.after;
			not_first: not a_cursor.is_last
		ensure -- from DS_DYNAMIC
			one_less: count = old count - 1

	wipe_out
			-- Remove all items from structure.
			-- (from DS_CONTAINER)
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
		ensure -- from DS_CONTAINER
			wipe_out: empty
		ensure -- from DS_CONTAINER
			wipe_out: empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize history to n items.
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
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: i_th (k) = old i_th (l);
			new_l: i_th (l) = old i_th (k)
	
feature -- Setting

	set_searcher (a_searcher: like list_searcher)
			-- Set searcher to a_searcher.
			-- (from DS_SEARCHABLE)
		require -- from DS_SEARCHABLE
			a_searcher_not_void: a_searcher /= void
		ensure -- from DS_SEARCHABLE
			searcher_set: list_searcher = a_searcher
	
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 LINEAR_CONTAINER
	after_definition: after = (index = count + 1);
	before_definition: before = (index = 0);
	isfirst_definition: isfirst = (not empty and then (index = 1));
	islast_definition: islast = (not empty and then (index = count));
		-- from SEQUENCIAL_CONTAINER
	empty_definition: empty = (count = 0);
	off_definition: off = (before or after);
	empty_constraint: empty implies off;
	count_range: 0 <= count and count <= capacity;
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: empty = (count = 0);
		-- from DS_SEARCHABLE
	searcher_not_void: list_searcher /= void;

end -- class LIST_ADAPTER