indexing
	description: "Indexed cursors for structure traversals"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

deferred class interface
	DS_INDEXED_CURSOR [G]

feature -- Access

	container: DS_TRAVERSABLE [G]
			-- Structure traversed
			-- (from DS_CURSOR)

	index: INTEGER
			-- Index of current position
		require
			valid_cursor: is_valid
		ensure
			valid_index: valid_index (Result)

	item: G
			-- Item at cursor position
			-- (from DS_CURSOR)
		require -- from DS_CURSOR
			valid_cursor: is_valid;
			not_off: not off
	
feature -- Status report

	is_valid: BOOLEAN
			-- Is cursor valid?
			-- (A cursor might become invalid if container
			-- has been modified during traversal.)
			-- (from DS_CURSOR)

	off: BOOLEAN
			-- Is there no item at cursor position?
			-- (from DS_CURSOR)
		require -- from DS_CURSOR
			valid_cursor: is_valid

	valid_index (i: INTEGER): BOOLEAN
			-- Is i a valid index value?
	
feature -- Cursor movement

	go_to (i: INTEGER)
			-- Move cursor to i-th position.
		require
			valid_cursor: is_valid;
			valid_index: valid_index (i)
		ensure
			moved: index = i
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from DS_CURSOR
	container_not_void: container /= void;
	empty_constraint: container.is_empty implies off;

end -- class DS_INDEXED_CURSOR