deferred class interface DS_INDEXABLE[G]

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_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

   first: G
      --  First item in container

      require
         not_empty: not is_empty
      ensure
         definition: Result = item(1)

   last: G
      --  Last item in container

      require
         not_empty: not is_empty
      ensure
         definition: Result = item(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

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;

end of deferred DS_INDEXABLE[G]