indexing
description: "Cursors for bilinked list traversals"
library: "Gobo Eiffel Structures Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
class interface
DS_BILINKED_LIST_CURSOR [G]
create
make (list: like container)
-- (from DS_LINKED_LIST_CURSOR)
require -- from DS_LINKED_LIST_CURSOR
list_not_void: list /= void
ensure -- from DS_LINKED_LIST_CURSOR
container_set: container = list;
before: before
feature -- Access
container: DS_BILINKED_LIST [G]
-- List traversed
index: INTEGER
-- Index of current position
-- (from DS_LINKED_LIST_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_LINKED_LIST_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_LINKED_LIST_CURSOR)
before: BOOLEAN
-- Is there no valid position to left of cursor?
-- (from DS_LINKED_LIST_CURSOR)
is_first: BOOLEAN
-- Is cursor on the first item?
-- (from DS_LINKED_LIST_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 the last item?
-- (from DS_LINKED_LIST_CURSOR)
require -- from DS_BILINEAR_CURSOR
valid_cursor: is_valid
ensure -- from DS_BILINEAR_CURSOR
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?
-- (from DS_LINKED_LIST_CURSOR)
off: BOOLEAN
-- Is there no item at cursor position?
-- (from DS_LINKED_LIST_CURSOR)
require -- from DS_CURSOR
valid_cursor: is_valid
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index value?
-- (from DS_BILINEAR_CURSOR)
feature -- Cursor movement
back
-- Move cursor to previous position.
require -- from DS_BILINEAR_CURSOR
valid_cursor: is_valid;
not_before: not before
finish
-- Move cursor to last position.
-- (from DS_LINKED_LIST_CURSOR)
require -- from DS_BILINEAR_CURSOR
valid_cursor: is_valid
ensure -- from DS_BILINEAR_CURSOR
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_LINKED_LIST_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_LINKED_LIST_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.
-- (from DS_BILINEAR_CURSOR)
require -- from DS_BILINEAR_CURSOR
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_LINKED_LIST_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
feature -- Element change
put (v: G)
-- Replace item at cursor position by v.
-- (from DS_LINKED_LIST_CURSOR)
require -- from DS_DYNAMIC_CURSOR
valid_cursor: is_valid;
not_off: not off
ensure -- from DS_DYNAMIC_CURSOR
replaced: item = v
feature -- Transformation
swap (other: like Current)
-- Exchange items at current and other positions.
-- Note: cursors may reference two different structures.
-- (from DS_DYNAMIC_CURSOR)
require -- from DS_DYNAMIC_CURSOR
valid_cursor: is_valid;
not_off: not off;
other_not_void: other /= void;
valid_other: other.is_valid;
other_not_off: not other.off
ensure -- from DS_DYNAMIC_CURSOR
new_item: item = old other.item;
new_other: other.item = old item
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from DS_BILINEAR_CURSOR
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_BILINKED_LIST_CURSOR