class interface P_LINKED_LIST[G]

creation
   make

feature(s) from P_ONEWAY_TRAVERSABLE
   --  Iteration

   iterator: P_ITERATOR[G]
      --  Iterator on this list.

      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)

      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_CONTAINER
   --  Status

   count: INTEGER
      --  Number of elements in the data structure.


   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   item: G
      --  Current item.
      --  Time: O(1)

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Remove all objects from the container.

      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_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
      --  Insertion sort.
      --  Time: O(count^2/4) comparisons; O(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_LIST
   --  Update 

   add (it: G)
      --  Add an item to the end of the list.
      --  Time: O(1)

      require
         writable: is_writable;
         not_void: not is_void(it)
      ensure
         keep_reference: item = it

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

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

   insert (it: G)
      --  Insert an item before the current item.
      --  Time: O(1)

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

   remove
      --  Remove the current item.
      --  Time: O(1)

      require
         writable: is_writable;
         not_empty: not is_empty;
         unlocked: not is_locked

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_LINKED_LIST
   make
      --  Remove all objects from the container.


invariant
   empty: is_empty = count = 0;
   valid_protect_count: protcount >= 0;
   protection: is_protected implies not is_writable;
   sym_current_first: current_node = Void = first_node = Void;
   sym_first_last: first_node = Void = last_node = Void;
   correct_bounds: not is_empty implies first_node.previous = Void and last_node.next = Void;

end of P_LINKED_LIST[G]