Class DS_INDEXABLE |

    indexing

>     description:

>         "Data structures that can be traversed and %
>         %modified through integer access"

>     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)"

    deferred class interface

>     DS_INDEXABLE [G]

    inherit

>     DS_SORTABLE [G]
>         DS_CONTAINER [G]

    feature {NONE} -- Initialization

>     make_default
>             -- Create an empty container.
>             -- (From DS_CONTAINER.)
>         deferred
>         ensure
>             empty: is_empty

    feature -- Access

>     infix "@", item (i: INTEGER): G
>             -- Item at index i
>         require
>             valid_index: 1 <= i and i <= count
>         deferred

>     first: G
>             -- First item in container
>         require
>             not_empty: not is_empty
>         deferred
>         ensure
>             definition: Result = item (1)

>     last: G
>             -- Last item in container
>         require
>             not_empty: not is_empty
>         deferred
>         ensure
>             definition: Result = item (count)

    feature -- Measurement

>     count: INTEGER
>             -- Number of items in container
>             -- (From DS_CONTAINER.)
>         deferred

    feature -- Status report

>     is_empty: BOOLEAN
>             -- Is container empty?
>             -- (From DS_CONTAINER.)

>     extendible (n: INTEGER): BOOLEAN
>             -- May container be extended with n items?
>         require
>             positive_n: n >= 0
>         deferred

>     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

    feature -- Comparison

>     is_equal (other: like Current): BOOLEAN
>             -- Is current container equal to other?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         deferred
>         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 container.
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>             type_identity: same_type (other)
>         deferred
>         ensure
>             is_equal: is_equal (other)

    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 -- Element change

>     put_first (v: G)
>             -- Add v to beginning of container.
>         require
>             extendible: extendible (1)
>         deferred
>         ensure
>             one_more: count = old count + 1
>             inserted: first = v

>     put_last (v: G)
>             -- Add v to end of container.
>         require
>             extendible: extendible (1)
>         deferred
>         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)
>         deferred
>         ensure
>             one_more: count = old count + 1
>             inserted: item (i) = v

>     force_first (v: G)
>             -- Add v to beginning of container.
>         deferred
>         ensure
>             one_more: count = old count + 1
>             inserted: first = v

>     force_last (v: G)
>             -- Add v to end of container.
>         deferred
>         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)
>         deferred
>         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
>         deferred
>         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)
>         deferred
>         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)
>         deferred
>         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)
>         deferred
>         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
>         deferred
>         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
>         deferred
>         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)
>         deferred
>         ensure
>             new_count: count = old count + other.count
>             same_order: (not other.is_empty) implies (item (i) = other.first)

    feature -- Removal

>     remove_first
>             -- Remove first item from container.
>         require
>             not_empty: not is_empty
>         deferred
>         ensure
>             one_less: count = old count - 1

>     remove_last
>             -- Remove last item from container.
>         require
>             not_empty: not is_empty
>         deferred
>         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
>         deferred
>         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
>         deferred
>         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
>         deferred
>         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)
>         deferred
>         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
>         deferred
>         ensure
>             new_count: count = n

>     keep_last (n: INTEGER)
>             -- Keep n last items in container.
>         require
>             valid_n: 0 <= n and n <= count
>         deferred
>         ensure
>             new_count: count = n

>     wipe_out
>             -- Remove all items from container.
>             -- (From DS_CONTAINER.)
>         deferred
>         ensure
>             wiped_out: is_empty

    invariant

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

    end -- class DS_INDEXABLE