class interface P_SEQUENCE_LIST[G]

creation
   make
      --  Remove all items.
      --  Time: O(1)


feature(s) from P_ONEWAY_TRAVERSABLE
   --  Iteration

   iterator: P_ITERATOR[G]
      --  Get a two-way iterator on this container.

      ensure
         done: Result /= Void; --  Result /= previous Result
         is_shallow_copy: 

   is_protected: BOOLEAN
      --  Is an iterator inside the data structure?


feature(s) from P_ONEWAY_TRAVERSABLE
   --  Lock status

   has_locked: BOOLEAN
      --  Does this container has one or more locked items?


   is_locked: BOOLEAN
      --  Is current item locked?
      --  Time: O(1) amortised [dictionary search]

      require
         meaningful: not is_empty
      ensure
         has_locked: Result = true implies has_locked

feature(s) from P_ONEWAY_TRAVERSABLE
   --  General (from P_CONTAINER)

   is_writable: BOOLEAN
      --  Is the structure writable?


feature(s) from P_SORTABLE
   --  Order relation

   has_order: BOOLEAN
      --  Does this container has an order relation defined?


   set_order (ord_rel: P_ORDER_RELATION[G])
      --  Set the order relation which will be used 
      --  when sorting. The relation stays the same when 
      --  the container is reset.

      require
         valid: ord_rel /= Void
      ensure
         keep_reference: has_order

feature(s) from P_SORTABLE
   --  Sorting

   sort
      --  Selection sort.
      --  Time: O(target.count^2) comparisons; O(target.count) swaps

      require
         has_order: has_order;
         writable: is_writable
      ensure
         sorted: is_sorted

   is_sorted: BOOLEAN
      --  Is the container sorted?
      --  Time: O(target.count)

      require
         has_order: has_order
      ensure
         empty_sorted: is_empty implies Result

feature(s) from P_SEARCHABLE
   --  Search

   value_search (x: G)
      --  Search items in the container which are of equal value (as defined 
      --  by the is_equal routine) with 'x'.
      --  Time: O(count)

      require
         readable: is_readable

   found: BOOLEAN
      --  Result of the last search operation.


   found_count: INTEGER
      --  Number of items found during the last search.

      require
         meaningful: found = true
      ensure
         meaningful: Result >= 1

feature(s) from P_CONTAINER
   --  Status

   count: INTEGER
      --  Quantity of items in the list.


   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   item: G
      --  Get current item.
      --  Time: O(1)

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Remove all items.
      --  Time: O(1)

      require
         writable: is_writable
      ensure
         done: is_empty

feature(s) from P_CONTAINER
   --  Output

   out: STRING
      --  String representation.

      ensure
         is_copy:  --  new string

feature(s) from P_CONTAINER
   --  Utility

   is_void (x: ANY): BOOLEAN
      --  Void assertion for generic parameters.


feature(s) from P_LIST
   --  Update 

   add (citem: G)
      --  Add item at the end of the list.
      --  Added item becomes current.
      --  Time: O(1) amortised

      require
         writable: is_writable;
         not_void: not is_void(citem)
      ensure
         in_container: container.item(count) = citem;
         count_ok: count = old count + 1;
         keep_reference: item = citem

   replace (citem: G)
      --  Replace current item.
      --  Time: O(1)

      require
         writable: is_writable;
         not_empty: not is_empty;
         not_void: not is_void(citem)
      ensure
         keep_reference: item = citem

   insert (citem: G)
      --  Insert item at current position, and push all the following items. 
      --  Time: O(count)

      require
         writable: is_writable;
         not_empty: not is_empty;
         not_void: not is_void(citem)
      ensure
         done: item = citem;
         count_ok: count = old count + 1;
         keep_reference: item = citem

   remove
      --  Remove current item.
      --  Time: O(count) amortised

      require
         writable: is_writable;
         not_empty: not is_empty;
         unlocked: not is_locked
      ensure
         count_ok: count = old count - 1

feature(s) from P_LIST
   --  Duplication

   copy (other: like Current)
      --  GENERAL's copy.
      --  Time: O(other.count)

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

feature(s) from P_LIST
   --  Comparison

   is_equal (other: like Current): BOOLEAN
      --  GENERAL's equality relation (requires covariant arguments).
      --  Time: O(count)

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

   is_equal_list (other: P_LIST[G]): BOOLEAN
      --  Compare two lists which can be of different dynamic type.
      --  Time: O(count)

      require
         valid: other /= Void

feature(s) from P_LIST
   --  Conversion

   from_list (other: P_LIST[G])
      --  Convert from another list.
      --  Note: The previous contents of this list is deleted.
      --  Time: O(other.count)

      require
         valid: other /= Void
      ensure
         done: is_equal_list(other); --  keep copy of items.
         keep_reference: 

   from_array (other: ARRAY[G])
      --  Convert from an ARRAY.
      --  Note: The previous contents of this list is deleted.
      --  Time: O(other.count)

      require
         valid: other /= Void; --  for_all other.item, other.item /= Void
         not_void: 
      ensure
         done: other.count = count; --  keep copy of items.
         keep_reference: 

   from_iterable (it: P_ONEWAY_ITERATOR[G])
      --  Convert from a one way linear iterable container.
      --  Note: The previous contents of this list is deleted.
      --  Time: O("it.count")

      require
         valid: it /= Void;
         initialised: it.outside
      ensure
         keep_reference:  --  keep copy of items.

   to_array: ARRAY[G]
      --  Convert list to ARRAY.
      --  Time: O(count)

      ensure
         done: is_empty = Result = Void; --  new array, same items.
         is_shallow_copy: 

feature(s) from P_LIST
   --  Concatenation

   append (other: P_LIST[G])
      --  Append other container to current.
      --  Time: O(other.count)

      require
         valid: other /= Void
      ensure
         keep_reference:  --  keep copy of items.

   append_iterable (it: P_ONEWAY_ITERATOR[G])
      --  Append the items from a linear iterator.
      --  Time: O("it.count")

      require
         valid_iterator: it /= Void;
         initialised: it.outside
      ensure
         keep_reference:  --  keep copy of items.

feature(s) from P_LIST
   --  Search

   equality_search (x: G)
      --  Search items in the container which are equal (as defined 
      --  by the = operator) with 'x'.
      --  Time: O(count)

      require
         readable: is_readable

feature(s) from P_SEQUENCE
   --  Update

   set_index (i: INTEGER)
      --  Set current item to position 'i'.
      --  Time: O(1)

      require
         not_empty: not is_empty;
         index_low: i >= 1;
         index_up: i <= count

feature(s) from P_SEQUENCE
   --  Status

   index: INTEGER
      --  Current index.
      --  Time: O(1)

      require
         not_empty: not is_empty
      ensure
         valid: Result >= 1 and Result <= count

feature(s) from P_SEQUENCE_LIST
   --  Creation

   make
      --  Remove all items.
      --  Time: O(1)


invariant
   empty: is_empty = count = 0;
   valid_protect_count: protcount >= 0;
   protection: is_protected implies not is_writable;
   valid_current: not is_empty implies current_item >= 1 and current_item <= count;
   good_container: container.lower = 1;
   big_container: count /= 0 implies container.upper >= count;
   small_container: count /= 0 implies container.count // Grow_factor <= Default_size + count;

end of P_SEQUENCE_LIST[G]