indexing
description: "Cursors for structures that may be traversed forward and backward"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
deferred class interface
DS_BILINEAR_CURSOR [G]
feature -- Access
container: DS_BILINEAR [G]
-- Structure to be traversed
index: INTEGER
-- Index of current position
-- (from DS_INDEXED_CURSOR)
require -- from DS_INDEXED_CURSOR
valid_cursor: is_valid
ensure -- from DS_INDEXED_CURSOR
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
after: BOOLEAN
-- Is there no valid position to right of cursor?
-- (from DS_LINEAR_CURSOR)
require -- from DS_LINEAR_CURSOR
valid_cursor: is_valid
before: BOOLEAN
-- Is there no valid position to left of cursor?
require
valid_cursor: is_valid
is_first: BOOLEAN
-- Is cursor on first item?
-- (from DS_LINEAR_CURSOR)
require -- from DS_LINEAR_CURSOR
valid_cursor: is_valid
ensure -- from DS_LINEAR_CURSOR
not_empty: Result implies not container.is_empty;
not_off: Result implies not off;
definition: Result implies (item = container.first)
is_last: BOOLEAN
-- Is cursor on last item?
require
valid_cursor: is_valid
ensure
not_empty: Result implies not container.is_empty;
not_off: Result implies not off;
definition: Result implies (item = container.last)
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?
require -- from DS_CURSOR
valid_cursor: is_valid
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index value?
feature -- Cursor movement
back
-- Move cursor to previous position.
require
valid_cursor: is_valid;
not_before: not before
finish
-- Move cursor to last position.
require
valid_cursor: is_valid
ensure
empty_behavior: container.is_empty implies before;
not_empty_behavior: not container.is_empty implies is_last
forth
-- Move cursor to next position.
-- (from DS_LINEAR_CURSOR)
require -- from DS_LINEAR_CURSOR
valid_cursor: is_valid;
not_after: not after
go_to (i: INTEGER)
-- Move cursor to i-th position.
-- (from DS_INDEXED_CURSOR)
require -- from DS_INDEXED_CURSOR
valid_cursor: is_valid;
valid_index: valid_index (i)
ensure -- from DS_INDEXED_CURSOR
moved: index = i
search_back (v: G)
-- Move to first position at or before current
-- position where item and v are equal.
-- (Use searcher's comparison criterion from container.)
-- Move before if not found.
require
valid_cursor: is_valid;
not_off: not off or before
search_forth (v: G)
-- Move to first position at or after current
-- position where item and v are equal.
-- (Use searcher's comparison criterion from container.)
-- Move after if not found.
-- (from DS_LINEAR_CURSOR)
require -- from DS_LINEAR_CURSOR
valid_cursor: is_valid;
not_off: not off or after
start
-- Move cursor to first position.
-- (from DS_LINEAR_CURSOR)
require -- from DS_LINEAR_CURSOR
valid_cursor: is_valid
ensure -- from DS_LINEAR_CURSOR
empty_behavior: container.is_empty implies after;
not_empty_behavior: not container.is_empty implies is_first
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
not_both: not (after and before);
before_constraint: before implies off;
-- from DS_LINEAR_CURSOR
after_constraint: after implies off;
empty_property: container.is_empty implies off;
-- from DS_CURSOR
container_not_void: container /= void;
empty_constraint: container.is_empty implies off;
end -- class DS_BILINEAR_CURSOR