deferred class interface DS_LIST[G]
feature(s) from DS_TRAVERSABLE
-- Access
item_for_iteration: G
-- Item at internal cursor position
require
not_off: not off
new_cursor: DS_LIST_CURSOR[G]
-- New external cursor for traversal
ensure
cursor_not_void: Result /= Void;
valid_cursor: valid_cursor(Result)
feature(s) from DS_TRAVERSABLE
-- Status report
off: BOOLEAN
-- Is there no item at internal cursor position?
same_position (a_cursor: like new_cursor): BOOLEAN
-- Is internal cursor at same position as a_cursor?
require
a_cursor_not_void: a_cursor /= Void
valid_cursor (a_cursor: DS_CURSOR[G]): BOOLEAN
-- Is a_cursor a valid cursor?
require
a_cursor_not_void: a_cursor /= Void
feature(s) from DS_TRAVERSABLE
-- Cursor movement
go_to (a_cursor: like new_cursor)
-- Move internal cursor to a_cursor's position.
require
cursor_not_void: a_cursor /= Void;
valid_cursor: valid_cursor(a_cursor)
ensure
same_position: same_position(a_cursor)
feature(s) from DS_SEARCHABLE
-- Status report
has (v: G): BOOLEAN
-- Does container include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
ensure
not_empty: Result implies not is_empty
same_items (v, u: G): BOOLEAN
-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
same_equality_tester (other: DS_SEARCHABLE[G]): BOOLEAN
-- Does container use the same comparison
-- criterion as other?
require
other_not_void: other /= Void
feature(s) from DS_SEARCHABLE
-- Measurement
occurrences (v: G): INTEGER
-- Number of times v appears in container
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
ensure
positive: Result >= 0;
has: has(v) implies Result >= 1
feature(s) from DS_SEARCHABLE
-- Access
equality_tester: DS_EQUALITY_TESTER[G]
-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.
feature(s) from DS_SEARCHABLE
-- 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.
ensure
equality_tester_set: equality_tester = a_tester
feature(s) from DS_LINEAR
-- Access
first: G
-- First item in container
require
not_empty: not is_empty
require else
not_empty: not is_empty
ensure
definition: Result = item(1);
has_first: has(Result)
feature(s) from DS_LINEAR
-- Status report
is_first: BOOLEAN
-- Is internal cursor on first item?
ensure
not_empty: Result implies not is_empty;
not_off: Result implies not off;
definition: Result implies item_for_iteration = first
after: BOOLEAN
-- Is there no valid position to right of internal cursor?
feature(s) from DS_LINEAR
-- Cursor movement
start
-- Move internal cursor to first position.
ensure
empty_behavior: is_empty implies after;
not_empty_behavior: not is_empty implies is_first
forth
-- Move internal cursor to next position.
require
not_after: not after
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.
require
not_off: not off or after
go_after
-- Move cursor to after position.
ensure
after: after
feature(s) from DS_CONTAINER
-- Measurement
count: INTEGER
-- Number of items in container
feature(s) from DS_CONTAINER
-- Status report
is_empty: BOOLEAN
-- Is container empty?
feature(s) from DS_CONTAINER
-- Comparison
is_equal (other: like Current): BOOLEAN
-- Is current container equal to other?
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
feature(s) from DS_CONTAINER
-- Removal
wipe_out
-- Remove all items from container.
ensure
wiped_out: is_empty
feature(s) from DS_SORTABLE
-- Status report
sorted (a_sorter: DS_SORTER[G]): BOOLEAN
-- Is container sorted according to a_sorter's criterion?
require
a_sorter_not_void: a_sorter /= Void
feature(s) from DS_SORTABLE
-- Sort
sort (a_sorter: DS_SORTER[G])
-- Sort container using a_sorter's algorithm.
require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted(a_sorter)
feature(s) from DS_BILINEAR
-- Access
last: G
-- Last item in container
require
not_empty: not is_empty
require else
not_empty: not is_empty
ensure
definition: Result = item(count);
has_last: has(Result)
feature(s) from DS_BILINEAR
-- Status report
is_last: BOOLEAN
-- Is internal cursor on last item?
ensure
not_empty: Result implies not is_empty;
not_off: Result implies not off;
definition: Result implies item_for_iteration = last
before: BOOLEAN
-- Is there no valid position to left of internal cursor?
feature(s) from DS_BILINEAR
-- Cursor movement
finish
-- Move internal cursor to last position.
ensure
empty_behavior: is_empty implies before;
not_empty_behavior: not is_empty implies is_last
back
-- Move internal cursor to previous position.
require
not_before: not before
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.
require
not_off: not off or before
go_before
-- Move cursor to before position.
ensure
before: before
feature(s) from DS_INDEXABLE
-- Access
infix "@" (i: INTEGER): G
-- Item at index i
require
valid_index: 1 <= i and i <= count
feature(s) from DS_INDEXABLE
-- Access
item (i: INTEGER): G
-- Item at index i
require
valid_index: 1 <= i and i <= count
feature(s) from DS_INDEXABLE
-- Status report
extendible (n: INTEGER): BOOLEAN
-- May container be extended with n items?
require
positive_n: n >= 0
feature(s) from DS_INDEXABLE
-- Element change
put_first (v: G)
-- Add v to beginning of container.
require
extendible: extendible(1)
ensure
one_more: count = old count + 1;
inserted: first = v
put_last (v: G)
-- Add v to end of container.
require
extendible: extendible(1)
ensure
one_more: count = old count + 1;
inserted: last = v
put (v: G; i: INTEGER)
-- Add v at i-th position.
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 container.
ensure
one_more: count = old count + 1;
inserted: first = v
force_last (v: G)
-- Add v to end of container.
ensure
one_more: count = old count + 1;
inserted: last = v
force (v: G; i: INTEGER)
-- Add v at i-th position.
require
valid_index: 1 <= i and i <= count + 1
ensure
one_more: count = old count + 1;
inserted: item(i) = v
replace (v: G; i: INTEGER)
-- Replace item at i-th position by v.
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.
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 container.
-- Keep items of other in the same order.
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 container.
-- Keep items of other in the same order.
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 (other: DS_LINEAR[G]; i: INTEGER)
-- Add items of other at i-th position.
-- Keep items of other in the same order.
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 container.
-- Keep items of other in the same order.
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 container.
-- Keep items of other in the same order.
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 (other: DS_LINEAR[G]; i: INTEGER)
-- Add items of other at i-th position.
-- Keep items of other in the same order.
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(s) from DS_INDEXABLE
-- Removal
remove_first
-- Remove first item from container.
require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_last
-- Remove last item from container.
require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove (i: INTEGER)
-- Remove item at i-th position.
require
not_empty: not is_empty;
valid_index: 1 <= i and i <= count
ensure
one_less: count = old count - 1
prune_first (n: INTEGER)
-- Remove n first items from container.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_last (n: INTEGER)
-- Remove n last items from container.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune (n: INTEGER; i: INTEGER)
-- Remove n items at and after i-th position.
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 container.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
keep_last (n: INTEGER)
-- Keep n last items in container.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
feature(s) from DS_LIST
-- Access
index: INTEGER
-- Index of current internal cursor position
ensure
valid_index: valid_index(Result)
feature(s) from DS_LIST
-- Status report
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index value?
ensure
definition: Result = (0 <= i and i <= count + 1)
feature(s) from DS_LIST
-- Cursor movement
go_i_th (i: INTEGER)
-- Move internal cursor to i-th position.
require
valid_index: valid_index(i)
ensure
moved: index = i
feature(s) from DS_LIST
-- Element change
put_left (v: G)
-- Add v to left of internal cursor position.
-- Do not move cursors.
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).)
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.
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).)
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
force_left (v: G)
-- Add v to left of internal cursor position.
-- Do not move cursors.
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.
-- Do not move cursors.
-- (Synonym of a_cursor.force_left (v).)
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.
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.
-- Do not move cursors.
-- (Synonym of a_cursor.force_right (v).)
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
replace_at (v: G)
-- Replace item at internal cursor position by v.
-- Do not move cursors.
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).)
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
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.
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).)
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.
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).)
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
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.
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.
-- Do not move cursors.
-- (Synonym of a_cursor.append_left (other).)
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.
-- Do not move cursors.
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.
-- Do not move cursors.
-- (Synonym of a_cursor.append_right (other).)
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
feature(s) from DS_LIST
-- Removal
remove_at
-- Remove item at internal cursor position.
-- Move any cursors at this position forth.
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.)
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_left
-- Remove item to left of internal cursor position.
-- Move any cursors at this position forth.
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.)
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.
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.)
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_left (n: INTEGER)
-- Remove n items to left of internal cursor position.
-- Move all cursors off.
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).)
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.
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).)
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
delete (v: G)
-- Remove all occurrences of v.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move all cursors off.
ensure
deleted: not has(v);
new_count: count = old count - occurrences(v)
invariant
positive_count: count >= 0;
empty_definition: is_empty = count = 0;
empty_constraint: is_empty implies off;
internal_cursor_not_void: internal_cursor /= Void;
valid_internal_cursor: valid_cursor(internal_cursor);
after_constraint: after implies off;
not_both: not (after and before);
before_constraint: before implies off;
end of deferred DS_LIST[G]