| Class DS_ARRAYED_LIST |
  |
indexing
description:
"Lists implemented with arrays"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobosoft.com>"
copyright: "Copyright (c) 1999-2001, Eric Bezault and others"
license: "MIT License"
class interface
DS_ARRAYED_LIST [G]
inherit
DS_LIST [G]
DS_BILINEAR [G]
DS_LINEAR [G]
DS_TRAVERSABLE [G]
DS_CONTAINER [G]
DS_SEARCHABLE [G]
DS_CONTAINER [G]
DS_INDEXABLE [G]
DS_SORTABLE [G]
DS_CONTAINER [G]
DS_RESIZABLE [G]
DS_CONTAINER [G]
create
make (n: INTEGER)
-- Create an empty list and allocate
-- memory space for at least n items.
-- Use `=' as comparison criterion.
require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
make_equal (n: INTEGER)
-- Create an empty list and allocate
-- memory space for at least n items.
-- Use equal as comparison criterion.
require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
make_from_linear (other: DS_LINEAR [G])
-- Create a new list and fill it with items of other.
-- Use `=' as comparison criterion.
require
other_not_void: other /= Void
ensure
count_set: count = other.count
capacity_set: capacity = count
before: before
make_default
-- Create an empty list and allocate memory
-- space for at least default_capacity items.
-- Use `=' as comparison criterion.
-- (From DS_CONTAINER.)
ensure
empty: is_empty
capacity_set: capacity = default_capacity
before: before
feature -- Access
infix "@", item (i: INTEGER): G
-- Item at index i
-- (Performance: O(1).)
-- (From DS_INDEXABLE.)
require
valid_index: 1 <= i and i <= count
item_for_iteration: G
-- Item at internal cursor position
-- (Performance: O(1).)
-- (From DS_TRAVERSABLE.)
require
not_off: not off
first: G
-- First item in list
-- (Performance: O(1).)
-- (From DS_LINEAR and DS_INDEXABLE.)
require
not_empty: not is_empty
ensure
has_first: has (Result)
definition: Result = item (1)
last: G
-- Last item in list
-- (Performance: O(1).)
-- (From DS_BILINEAR and DS_INDEXABLE.)
require
not_empty: not is_empty
ensure
has_last: has (Result)
definition: Result = item (count)
new_cursor: DS_ARRAYED_LIST_CURSOR [G]
-- New external cursor for traversal
-- (From DS_TRAVERSABLE.)
ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)
index: INTEGER
-- Index of current internal cursor position
-- (Performance: O(1).)
-- (From DS_LIST.)
ensure
valid_index: valid_index (Result)
equality_tester: DS_EQUALITY_TESTER [G]
-- Equality tester;
-- A void equality tester means that `='
-- will be used as comparison criterion.
-- (From DS_SEARCHABLE.)
feature -- Measurement
count: INTEGER
-- Number of items in list
-- (Performance: O(1).)
-- (From DS_CONTAINER.)
capacity: INTEGER
-- Maximum number of items in list
-- (From DS_RESIZABLE.)
default_capacity: INTEGER
-- Initial capacity in make_default
-- (Default value: 10)
-- (From DS_RESIZABLE.)
ensure
default_capacity_positive: Result >= 0
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 -- Status report
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 list empty?
-- (From DS_CONTAINER.)
is_full: BOOLEAN
-- Is list full?
-- (From DS_RESIZABLE.)
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)
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.)
off: BOOLEAN
-- Is there no item at internal cursor position?
-- (From DS_TRAVERSABLE.)
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
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))
extendible (n: INTEGER): BOOLEAN
-- May list be extended with n items?
-- (From DS_INDEXABLE.)
require
positive_n: n >= 0
ensure
enough_space: Result implies (capacity >= count + n)
sorted (a_sorter: DS_SORTER [G]): BOOLEAN
-- Is list sorted according to a_sorter's criterion?
-- (From DS_SORTABLE.)
require
a_sorter_not_void: a_sorter /= 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_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
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.)
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is list equal to other?
-- Do not take cursor positions, capacity
-- nor equality_tester into account.
-- (Performance: O(count).)
-- (From GENERAL.)
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_equal (Current)
same_count: Result implies count = other.count
feature -- Duplication
copy (other: like Current)
-- Copy other to current list.
-- Move all cursors off (unless other = Current).
-- (Performance: O(other.count).)
-- (From GENERAL.)
require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
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 -- Sort
sort (a_sorter: DS_SORTER [G])
-- Sort list using a_sorter's algorithm.
-- (From DS_SORTABLE.)
require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)
feature -- Cursor movement
start
-- Move internal cursor to first position.
-- (Performance: O(1).)
-- (From DS_LINEAR.)
ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first
finish
-- Move internal cursor to last position.
-- (Performance: O(1).)
-- (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.
-- (Performance: O(1).)
-- (From DS_LINEAR.)
require
not_after: not after
back
-- Move internal cursor to previous position.
-- (Performance: O(1).)
-- (From DS_BILINEAR.)
require
not_before: not 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
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
go_after
-- Move cursor to after position.
-- (Performance: O(1).)
-- (From DS_LINEAR.)
ensure
after: after
go_before
-- Move cursor to before position.
-- (Performance: O(1).)
-- (From DS_BILINEAR.)
ensure
before: before
go_to (a_cursor: like new_cursor)
-- Move internal cursor to a_cursor's position.
-- (Performance: O(1).)
-- (From DS_TRAVERSABLE.)
require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
go_i_th (i: INTEGER)
-- Move internal cursor to i-th position.
-- (Performance: O(1).)
-- (From DS_LIST.)
require
valid_index: valid_index (i)
ensure
moved: index = i
feature -- Element change
put_first (v: G)
-- Add v to beginning of list.
-- Do not move cursors.
-- (Performance: O(count).)
-- (From DS_INDEXABLE.)
require
extendible: extendible (1)
ensure
one_more: count = old count + 1
inserted: first = v
put_last (v: G)
-- Add v to end of list.
-- Do not move cursors.
-- (Performance: O(1).)
-- (From DS_INDEXABLE.)
require
extendible: extendible (1)
ensure
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.
-- (Performance: O(count-index).)
-- (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)
-- Add v to left of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_left (v).)
-- (Performance: O(count-a_cursor.index).)
-- (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.
-- (Performance: O(count-index).)
-- (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)
-- Add v to right of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_right (v).)
-- (Performance: O(count-a_cursor.index).)
-- (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
put (v: G; i: INTEGER)
-- Add v at i-th position.
-- Do not move cursors.
-- (Performance: O(count-i).)
-- (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
force_first (v: G)
-- Add v to beginning of list.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count)[+resizing].)
-- (From DS_INDEXABLE.)
ensure
one_more: count = old count + 1
inserted: first = v
force_last (v: G)
-- Add v to end of list.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(1)[+resizing].)
-- (From DS_INDEXABLE.)
ensure
one_more: count = old count + 1
inserted: last = v
force_left (v: G)
-- Add v to left of internal cursor position.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-index)[+resizing].)
-- (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)
-- Add v to left of a_cursor position.
-- Resize container if needed.
-- Do not move cursors.
-- (Synonym of a_cursor.force_left (v).)
-- (Performance: O(count-a_cursor.index)[+resizing].)
-- (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.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-index)[+resizing].)
-- (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)
-- Add v to right of a_cursor position.
-- Resize container if needed.
-- Do not move cursors.
-- (Synonym of a_cursor.force_right (v).)
-- (Performance: O(count-a_cursor.index)[+resizing].)
-- (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
force (v: G; i: INTEGER)
-- Add v at i-th position.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-i)[+resizing].)
-- (From DS_INDEXABLE.)
require
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
replace_at (v: G)
-- Replace item at internal cursor position by v.
-- Do not move cursors.
-- (Performance: O(1).)
-- (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 item at a_cursor position by v.
-- Do not move cursors.
-- (Synonym of a_cursor.replace (v).)
-- (Performance: O(1).)
-- (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
replace (v: G; i: INTEGER)
-- Replace item at i-th position by v.
-- Do not move cursors.
-- (Performance: O(1).)
-- (From DS_INDEXABLE.)
require
valid_index: 1 <= i and i <= count
ensure
same_count: count = old count
replaced: item (i) = v
swap (i, j: INTEGER)
-- Exchange items at indexes i and j.
-- Do not move cursors.
-- (Performance: O(1).)
-- (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)
extend_first (other: DS_LINEAR [G])
-- Add items of other to beginning of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(count+other.count).)
-- (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])
-- Add items of other to end of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(other.count).)
-- (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 (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.
-- (Performance: O(count-index+other.count).)
-- (From DS_LIST.)
require
other_not_void: other /= Void
extendible: extendible (other.count)
not_before: not before
ensure
new_count: count = old count + 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)
-- Add items of other to left of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_left (other).)
-- (Performance: O(count-a_cursor.index+other.count).)
-- (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 + 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.
-- (Performance: O(count-index+other.count).)
-- (From DS_LIST.)
require
other_not_void: other /= Void
extendible: extendible (other.count)
not_after: not after
ensure
new_count: count = old count + 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)
-- Add items of other to right of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_right (other).)
-- (Performance: O(count-a_cursor.index+other.count).)
-- (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 + other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
extend (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(count-i+other.count).)
-- (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)
append_first (other: DS_LINEAR [G])
-- Add items of other to beginning of list.
-- Keep items of other in the same order.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count+other.count)[+resizing].)
-- (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])
-- Add items of other to end of list.
-- Keep items of other in the same order.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(other.count)[+resizing].)
-- (From DS_INDEXABLE.)
require
other_not_void: other /= Void
ensure
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.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-index+other.count)[+resizing].)
-- (From DS_LIST.)
require
other_not_void: other /= Void
not_before: not before
ensure
new_count: count = old count + 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)
-- Add items of other to left of a_cursor position.
-- Keep items of other in the same order.
-- Resize container if needed.
-- Do not move cursors.
-- (Synonym of a_cursor.append_left (other).)
-- (Performance: O(count-a_cursor.index+other.count)[+resizing].)
-- (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 + 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.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-index+other.count)[+resizing].)
-- (From DS_LIST.)
require
other_not_void: other /= Void
not_after: not after
ensure
new_count: count = old count + 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)
-- Add items of other to right of a_cursor position.
-- Keep items of other in the same order.
-- Resize container if needed.
-- Do not move cursors.
-- (Synonym of a_cursor.append_right (other).)
-- (Performance: O(count-a_cursor.index+other.count)[+resizing].)
-- (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 + other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
append (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- Keep items of other in the same order.
-- Resize container if needed.
-- Do not move cursors.
-- (Performance: O(count-i+other.count)[+resizing].)
-- (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)
feature -- Removal
remove (i: INTEGER)
-- Remove item at i-th position.
-- Move any cursors at this position forth.
-- (Performance: O(count-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.
-- (Performance: O(count-index).)
-- (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-a_cursor.index).)
-- (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 first item from 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_last
-- Remove last item from 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_left
-- Remove item to left of internal cursor position.
-- Move any cursors at this position forth.
-- (Performance: O(count-index).)
-- (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_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_left.)
-- (Performance: O(count-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.
-- (Performance: O(count-index).)
-- (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(count-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_after: not a_cursor.after
not_last: not a_cursor.is_last
ensure
one_less: count = old count - 1
prune_first (n: INTEGER)
-- Remove n first 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_last (n: INTEGER)
-- Remove n last items from list.
-- Move all cursors off.
-- (Performance: O(1).)
-- (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.
-- (Performance: O(count-index).)
-- (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(count-a_cursor.index).)
-- (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.
-- (Performance: O(count-index-n).)
-- (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(count-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 <= (count - a_cursor.index)
ensure
new_count: count = old count - n
prune (n: INTEGER; i: INTEGER)
-- Remove n items at and after i-th position.
-- Move all cursors off.
-- (Performance: O(count-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
keep_first (n: INTEGER)
-- Keep n first items in list.
-- Move all cursors off.
-- (Performance: O(1).)
-- (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(n).)
-- (From DS_INDEXABLE.)
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
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^2).)
-- (From DS_LIST