Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

xml.tree

Class XM_LINKED_LIST


Direct ancestors

DS_LINKED_LIST

Known direct descendants

XM_COMPOSITE

Features

Invariants

indexing

description

Linked list with a routine called before adding an object

library

Gobo Eiffel XML Library

copyright

Copyright (c) 2003, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2003/05/11 22:35:25 $

revision

$Revision: 1.1 $

deferred class

XM_LINKED_LIST [G]

inherit

DS_LINKED_LIST

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [G]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

first: G

-- First item in list
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
index: INTEGER

-- Index of current internal cursor position

-- (From DS_LIST)

ensure
valid_index: valid_index (Result)
infix "@" (i: INTEGER): G

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item (i: INTEGER): G

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item_for_iteration: G

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
last: G

-- Last item in list
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_LINKED_LIST_CURSOR [G]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)

feature -- Measurement

count: INTEGER

-- Number of items in list
-- (Performance: O(1).)

-- (From DS_CONTAINER)

occurrences (v: G): INTEGER

-- Number of times v appears in list
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is list equal to other?
-- Do not take cursor positions nor
-- equality_tester into account.
-- (Performance: O(count).)

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of internal cursor?

-- (From DS_LINEAR)

before: BOOLEAN

-- Is there no valid position to left of internal cursor?

-- (From DS_BILINEAR)

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

extendible (n: INTEGER): BOOLEAN

-- May list be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
ensure then
definition: Result = True
has (v: G): BOOLEAN

-- Does list include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_first: BOOLEAN

-- Is internal cursor on first item?

-- (From DS_LINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = first)
is_last: BOOLEAN

-- Is internal cursor on last item?

-- (From DS_BILINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = last)
off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [G]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: G): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

same_position (a_cursor: like new_cursor): BOOLEAN

-- Is internal cursor at same position as a_cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
sorted (a_sorter: DS_SORTER [G]): BOOLEAN

-- Is container sorted according to a_sorter's criterion?

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
valid_cursor (a_cursor: DS_CURSOR [G]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_index (i: INTEGER): BOOLEAN

-- Is i a valid index value?

-- (From DS_LIST)

ensure
definition: Result = (0 <= i and i <= (count + 1))

feature -- Cursor movement

back

-- Move internal cursor to previous position.

-- (From DS_BILINEAR)

require
not_before: not before
finish

-- Move internal cursor to last position.

-- (From DS_BILINEAR)

ensure
empty_behavior: is_empty implies before
not_empty_behavior: not is_empty implies is_last
forth

-- Move internal cursor to next position.

-- (From DS_LINEAR)

require
not_after: not after
go_after

-- Move internal cursor to after position.

-- (From DS_LINEAR)

ensure
after: after
go_before

-- Move internal cursor to before position.

-- (From DS_BILINEAR)

ensure
before: before
go_i_th (i: INTEGER)

-- Move internal cursor to i-th position.

-- (From DS_LIST)

require
valid_index: valid_index (i)
ensure
moved: index = i
go_to (a_cursor: like new_cursor)

-- Move internal cursor to a_cursor's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
search_back (v: G)

-- Move internal cursor to first position at or before current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
not_off: not off or before
search_forth (v: G)

-- Move internal cursor to first position at or after current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
not_off: not off or after
start

-- Move internal cursor to first position.

-- (From DS_LINEAR)

ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first

feature -- Element change

append (other: DS_LINEAR [G]; i: INTEGER)

-- append with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
append_first (other: DS_LINEAR [G])

-- append_first with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
append_last (other: DS_LINEAR [G])

-- append_last with parent processing.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
append_left (other: DS_LINEAR [G])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
append_left_cursor (other: DS_LINEAR [G]; a_cursor: like new_cursor)

-- append_left_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
append_right (other: DS_LINEAR [G])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
append_right_cursor (other: DS_LINEAR [G]; a_cursor: like new_cursor)

-- append_right_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
extend (other: DS_LINEAR [G]; i: INTEGER)

-- extend with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
extend_first (other: DS_LINEAR [G])

-- extend_first with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
extend_last (other: DS_LINEAR [G])

-- extend_last with parent processing.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
extend_left (other: DS_LINEAR [G])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
extend_left_cursor (other: DS_LINEAR [G]; a_cursor: like new_cursor)

-- extend_left_cursor with parent processing.

-- (From DS_LIST)

require
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
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
extend_right (other: DS_LINEAR [G])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
extend_right_cursor (other: DS_LINEAR [G]; a_cursor: like new_cursor)

-- extend_right_cursor with parent processing.

-- (From DS_LIST)

require
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
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
force (v: G; i: INTEGER)

-- force with parent processing.

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
force_first (v: G)

-- force_first with parent processing.

-- (From DS_INDEXABLE)

ensure
one_more: count = old count + 1
inserted: first = v
force_last (v: G)

-- force_last with parent processing.

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
force_left (v: G)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_before: not before
ensure
one_more: count = old count + 1
force_left_cursor (v: G; a_cursor: like new_cursor)

-- force_left_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
force_right (v: G)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_after: not after
ensure
one_more: count = old count + 1
force_right_cursor (v: G; a_cursor: like new_cursor)

-- force_right_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
put (v: G; i: INTEGER)

-- put with parent processing.

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
put_first (v: G)

-- put_first with parent processing.

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
ensure
one_more: count = old count + 1
inserted: first = v
put_last (v: G)

-- put_last with parent processing.

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
put_left (v: G)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_before: not before
ensure
one_more: count = old count + 1
put_left_cursor (v: G; a_cursor: like new_cursor)

-- put_left_cursor with parent processing.

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
put_right (v: G)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_after: not after
ensure
one_more: count = old count + 1
put_right_cursor (v: G; a_cursor: like new_cursor)

-- put_right_cursor with parent processing.

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
replace (v: G; i: INTEGER)

-- replace with parent processing.

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
ensure
same_count: count = old count
replaced: item (i) = v
replace_at (v: G)

-- replace_at with parent processing.

-- (From DS_LIST)

require
not_off: not off
ensure
same_count: count = old count
replaced: item_for_iteration = v
replace_at_cursor (v: G; a_cursor: like new_cursor)

-- replace_at_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
same_count: count = old count
replaced: a_cursor.item = v
swap (i, j: INTEGER)

-- Exchange items at indexes i and j.
-- Do not move cursors.
-- (Performance: O(max(i,j)).)

-- (From DS_INDEXABLE)

require
valid_i: 1 <= i and i <= count
valid_j: 1 <= j and j <= count
ensure
same_count: count = old count
new_i: item (i) = old item (j)
new_j: item (j) = old item (i)

feature -- Removal

delete (v: G)

-- Remove all occurrences of v.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move all cursors off.
-- (Performance: O(count).)

-- (From DS_LIST)

ensure
deleted: not has (v)
new_count: count = old (count - occurrences (v))
keep_first (n: INTEGER)

-- Keep n first items in list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
keep_last (n: INTEGER)

-- Keep n last items in list.
-- Move all cursors off.
-- (Performance: O(count-n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER; i: INTEGER)

-- Remove n items at and after i-th position.
-- Move all cursors off.
-- (Performance: O(i+n).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
valid_n: 0 <= n and n <= (count - i + 1)
ensure
new_count: count = old count - n
prune_first (n: INTEGER)

-- Remove n first items from list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_last (n: INTEGER)

-- Remove n last items from list.
-- Move all cursors off.
-- (Performance: O(count-n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_left (n: INTEGER)

-- Remove n items to left of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n < index
ensure
new_count: count = old count - n
prune_left_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to left of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_left (n).)
-- (Performance: O(2*a_cursor.index-n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n < a_cursor.index
ensure
new_count: count = old count - n
prune_right (n: INTEGER)

-- Remove n items to right of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n <= (count - index)
ensure
new_count: count = old count - n
prune_right_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to right of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_right (n).)
-- (Performance: O(n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n <= (count - a_cursor.index)
ensure
new_count: count = old count - n
remove (i: INTEGER)

-- Remove item at i-th position.
-- Move any cursors at this position forth.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
valid_index: 1 <= i and i <= count
ensure
one_less: count = old count - 1
remove_at

-- Remove item at internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_off: not off
ensure
one_less: count = old count - 1
remove_at_cursor (a_cursor: like new_cursor)

-- Remove item at a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove.)
-- (Performance: O(count) if a_cursor.is_last, O(1) otherwise.)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
one_less: count = old count - 1
remove_first

-- Remove item at beginning of list.
-- Move any cursors at this position forth.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_last

-- Remove item at end of list.
-- Move any cursors at this position forth.
-- (Performance: O(count).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_left

-- Remove item to left of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_before: not before
not_first: not is_first
ensure
one_less: count = old count - 1
remove_left_cursor (a_cursor: like new_cursor)

-- Remove item to left of a_cusor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_left.)
-- (Performance: O(a_cursor.index).)

-- (From DS_LIST)

require
not_empty: not is_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
one_less: count = old count - 1
remove_right

-- Remove item to right of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_after: not after
not_last: not is_last
ensure
one_less: count = old count - 1
remove_right_cursor (a_cursor: like new_cursor)

-- Remove item to right of a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_right.)
-- (Performance: O(1).)

-- (From DS_LIST)

require
not_empty: not is_empty
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
not_last: not a_cursor.is_last
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from list.
-- Move all cursors off.
-- (Performance: O(1).)

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Copy other to current list.
-- Move all cursors off (unless other = Current).
-- (Performance: O(other.count).)

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
to_array: ARRAY [G]

-- Array containing the same items as current
-- container in the same order

-- (From DS_LINEAR)

ensure
to_array_not_void: Result /= Void
same_count: Result.count = count

feature {DS_CURSOR} -- Cursor implementation

add_traversing_cursor (a_cursor: like new_cursor)

-- Add a_cursor to the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
cursor_after (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to right of a_cursor?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_back (a_cursor: like new_cursor)

-- Move a_cursor to previous position.
-- (Performance: O(a_cursor.index).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_before: not cursor_before (a_cursor)
cursor_before (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to left of a_cursor?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_finish (a_cursor: like new_cursor)

-- Move a_cursor to last position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_before (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_last (a_cursor)
cursor_forth (a_cursor: like new_cursor)

-- Move a_cursor to next position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_after: not cursor_after (a_cursor)
cursor_go_after (a_cursor: like new_cursor)

-- Move a_cursor to after position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_after: cursor_after (a_cursor)
cursor_go_before (a_cursor: like new_cursor)

-- Move a_cursor to before position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_before: cursor_before (a_cursor)
cursor_go_i_th (a_cursor: like new_cursor; i: INTEGER)

-- Move a_cursor to i-th position.
-- (Performance: O(i).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
valid_index: valid_index (i)
ensure
moved: cursor_index (a_cursor) = i
cursor_go_to (a_cursor, other: like new_cursor)

-- Move a_cursor to other's position.
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: cursor_same_position (a_cursor, other)
cursor_index (a_cursor: like new_cursor): INTEGER

-- Index of a_cursor's current position
-- (Performance: O(count).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
valid_index: valid_index (Result)
cursor_is_first (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on first item?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = first)
cursor_is_last (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on last item?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = last)
cursor_item (a_cursor: like new_cursor): G

-- Item at a_cursor position
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_off (a_cursor: like new_cursor): BOOLEAN

-- Is there no item at a_cursor position?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_same_position (a_cursor, other: like new_cursor): BOOLEAN

-- Is a_cursor at same position as other?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
cursor_search_back (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or before its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.
-- (Performance: O(a_cursor.index).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_before (a_cursor)
cursor_search_forth (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or after its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_after (a_cursor)
cursor_start (a_cursor: like new_cursor)

-- Move a_cursor to first position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_after (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_first (a_cursor)
remove_traversing_cursor (a_cursor: like new_cursor)

-- Remove a_cursor from the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature -- Sort

sort (a_sorter: DS_SORTER [G])

-- Sort container using a_sorter's algorithm.

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester

feature {DS_LINKED_LIST, DS_LINKED_LIST_CURSOR} -- Implementation

first_cell: DS_LINKABLE [G]

-- First cell in list

-- (From DS_LINKED_LIST)

last_cell: like first_cell

-- Last cell in list

-- (From DS_LINKED_LIST)

invariant

first_cell: is_empty = (first_cell = Void)
last_cell: is_empty = (last_cell = Void)
last_constraint: last_cell /= Void implies last_cell.right = Void

-- From DS_BILINEAR
not_both: initialized implies (not (after and before))
before_constraint: initialized implies (before implies off)

-- From DS_LINEAR
after_constraint: initialized implies (after implies off)

empty_constraint: initialized implies (is_empty implies off)
internal_cursor_not_void: initialized implies (internal_cursor /= Void)
valid_internal_cursor: initialized implies valid_cursor (internal_cursor)

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end