indexing
description: "Structures that can be traversed"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
deferred class interface
DS_TRAVERSABLE [G]
feature -- Access
new_cursor: DS_CURSOR [G]
-- New cursor for traversal
ensure
cursor_not_void: Result /= void;
valid_cursor: valid_cursor (Result)
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
feature -- Status report
is_empty: BOOLEAN
-- Is structure empty?
-- (from DS_CONTAINER)
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.)
require
a_cursor_not_void: a_cursor /= void
ensure
is_valid: Result implies a_cursor.is_valid
feature -- Removal
wipe_out
-- Remove all items from structure.
-- (from DS_CONTAINER)
ensure -- from DS_CONTAINER
wipe_out: is_empty
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_TRAVERSABLE