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:    "Eiffel Forum License v2 (see forum.txt)"

    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]

    creation

>     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.)
>         ensure
>             deleted: not has (v)
>             new_count: count = old (count - occurrences (v))

>     wipe_out
>             -- Remove all items from list.
>             -- Move all cursors off.
>             -- (Performance: O(1).)
>             -- (From DS_CONTAINER.)
>         ensure
>             wiped_out: is_empty

    feature -- Resizing

>     resize (n: INTEGER)
>             -- Resize list so that it can contain
>             -- at least n items. Do not lose any item.
>             -- (From DS_RESIZABLE.)
>         require
>             n_large_enough: n >= capacity
>         ensure
>             capacity_set: capacity = n

    invariant

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

>     empty_constraint: is_empty implies off
>         -- (From DS_TRAVERSABLE.)

>     after_constraint: after implies off
>         -- (From DS_LINEAR.)

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

>     count_constraint: count <= capacity
>     full_definition: is_full = (count = capacity)
>         -- (From DS_RESIZABLE.)

    end -- class DS_ARRAYED_LIST