deferred class interface DS_LINEAR[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_TRAVERSABLE
   --  Access

   item_for_iteration: G
      --  Item at internal cursor position

      require
         not_off: not off

   new_cursor: DS_LINEAR_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
      ensure
         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

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;

end of deferred DS_LINEAR[G]