class interface TWO_WAY_LINKED_LIST[E]
   --  
   --  Two way linked list with internal automatic memorization of 
   --  the last access.
   -- 

creation
   make
      --  Make an empty list;

      ensure
         count = 0

   from_collection (model: COLLECTION[like item])
      --  Initialize the current object with the contents of model.

      require
         model /= Void
      ensure
         count = model.count

feature(s) from COLLECTION
   --  Indexing :

   lower: INTEGER
      --  Lower index bound is frozen.


   upper: INTEGER
      --  Memorized upper index bound.


   valid_index (index: INTEGER): BOOLEAN
      --  True when index is valid (ie. inside actual 
      --  bounds of the collection).

      ensure
         Result = (lower <= index and then index <= upper)

feature(s) from COLLECTION
   --  Counting :

   count: INTEGER
      --  Number of elements actually stored in the collection.

      ensure
         Result = upper - lower + 1

   empty: BOOLEAN
      --  Is collection empty?


feature(s) from COLLECTION
   --  Accessing :

   item (index: INTEGER): E
      --  Item at position index.

      require
         valid_index(index)

feature(s) from COLLECTION
   --  Accessing :

   infix "@" (index: INTEGER): E
      --  Item at position index.

      require
         valid_index(index)

   first: like item
      --  The very first item.

      require
         count >= 1
      ensure
         Result = item(lower)

   last: like item
      --  The last item.

      require
         count >= 1
      ensure
         Result = item(upper)

feature(s) from COLLECTION
   --  Writing :

   put (element: like item; index: INTEGER)
      --  Put element at position index.

      require
         valid_index(index)
      ensure
         item(index) = element;
         count = old count

   swap (i1, i2: INTEGER)
      --  Swap item at index i1 with item at index i2.

      require
         valid_index(i1);
         valid_index(i2)
      ensure
         item(i1) = old item(i2);
         item(i2) = old item(i1);
         count = old count

   set_all_with (v: like item)
      --  Set all items with value v.

      ensure
         count = old count

   set_slice_with (v: like item; lower_index, upper_index: INTEGER)
      --  Set all items in range [lower_index .. upper_index] with v.

      require
         lower_index <= upper_index;
         valid_index(lower_index);
         valid_index(upper_index)
      ensure
         count = old count

   clear_all
      --  Set all items to default values.
      --  The count is not affected (see also clear).

      ensure
         count = old count;
         all_cleared

feature(s) from COLLECTION
   --  Adding :

   add_first (element: like item)
      --  Add a new item in first position : count is increased by 
      --  one and all other items are shifted right.

      ensure
         upper = 1 + old upper;
         first = element;
         count = 1 + old count;
         lower = old lower;
         upper = 1 + old upper

   add_last (element: like item)
      --  Add a new item at the end : count is increased by one.

      ensure
         last = element;
         count = 1 + old count;
         lower = old lower;
         upper = 1 + old upper

   add (element: like item; index: INTEGER)
      --  Add a new element at rank index : count is increased 
      --  by one and range [index .. upper] is shifted right
      --  by one position.

      require
         lower <= index;
         index <= upper + 1
      ensure
         item(index) = element;
         count = 1 + old count;
         upper = 1 + old upper

feature(s) from COLLECTION
   --  Modification :

   force (element: E; index: INTEGER)
      --  Put element at position index. Collection is
      --  resized if index is not inside current bounds.
      --  New bounds are initialized with default values.

      require
         index >= lower
      ensure
         valid_index(index);
         item(index) = element

   from_collection (model: COLLECTION[like item])
      --  Initialize the current object with the contents of model.

      require
         model /= Void
      ensure
         count = model.count

feature(s) from COLLECTION
   --  Removing :

   remove_first
      --  Remove the first element of the collection.

      require
         not empty
      ensure
         count = old count - 1;
         lower = old lower + 1 xor upper = old upper - 1

   remove (index: INTEGER)
      --  Remove the item at position index. Followings items
      --  are shifted left by one position.

      require
         valid_index(index)
      ensure
         count = old count - 1;
         upper = old upper - 1

   remove_last
      --  Remove the last item.

      require
         not empty
      ensure
         count = old count - 1;
         upper = old upper - 1

   clear
      --  Discard all items in order to make it empty.
      --  See also clear_all.

      ensure
         upper = 0;
         empty

feature(s) from COLLECTION
   --  Looking and Searching :

   has (x: like item): BOOLEAN
      --  Look for x using equal for comparison.
      --  Also consider fast_has to choose the most appropriate.


   fast_has (x: like item): BOOLEAN
      --  Look for x using basic = for comparison.
      --  Also consider has to choose the most appropriate.


   index_of (x: like item): INTEGER
      --  Give the index of the first occurrence of element using
      --  is_equal for comparison.
      --  Answer upper + 1 when element is not inside.
      --  Also consider fast_index_of to choose the most appropriate.

      ensure
         lower <= Result;
         Result <= upper + 1;
         Result <= upper implies equal(x,item(Result))

   fast_index_of (x: like item): INTEGER
      --  Give the index of the first occurrence of element using
      --  basic = for comparison.
      --  Answer upper + 1 when element is not inside.
      --  Also consider index_of to choose the most appropriate.

      ensure
         lower <= Result;
         Result <= upper + 1;
         Result <= upper implies x = item(Result)

feature(s) from COLLECTION
   --  Looking and comparison :

   all_cleared: BOOLEAN
      --  Are all items set to the default value ?


   nb_occurrences (element: like item): INTEGER
      --  Number of occurrences of element using equal for comparison.
      --  Also consider fast_nb_occurences to choose the most appropriate.

      ensure
         Result >= 0

   fast_nb_occurrences (element: like item): INTEGER
      --  Number of occurrences of element using basic = for comparison.
      --  Also consider nb_occurences to choose the most appropriate.

      ensure
         Result >= 0

feature(s) from COLLECTION
   --  Printing :

   fill_tagged_out_memory
      --  Append a viewable information in tagged_out_memory in 
      --  order to affect the behavior of out, tagged_out, etc.


feature(s) from COLLECTION
   --  Other Features :

   replace_all (old_value, new_value: like item)
      --  Replace all occurences of the element old_value by new_value 
      --  using equal for comparison.
      --  See also fast_replace_all to choose the apropriate one.

      ensure
         count = old count;
         nb_occurrences(old_value) = 0

   fast_replace_all (old_value, new_value: like item)
      --  Replace all occurences of the element old_value by new_value 
      --  using operator = for comparison.
      --  See also replace_all to choose the apropriate one.

      ensure
         count = old count;
         fast_nb_occurrences(old_value) = 0

   move (lower_index, upper_index, distance: INTEGER)
      --  Move range lower_index .. upper_index by distance 
      --  positions. Negative distance moves towards lower indices.
      --  Free places get default values.

      require
         lower_index <= upper_index;
         valid_index(lower_index);
         valid_index(lower_index + distance);
         valid_index(upper_index);
         valid_index(upper_index + distance)
      ensure
         count = old count

   slice (low, up: INTEGER): like Current
      --  Create a new collection initialized with elements of
      --  range low..up. Result has the same dynamic type 
      --  as Current collection. The lower index of the new 
      --  collection is the same as lower of Current.

      require
         valid_index(low);
         valid_index(up);
         low <= up
      ensure
         same_type(Result);
         Result.count = up - low + 1;
         Result.lower = lower

feature(s) from TWO_WAY_LINKED_LIST
   make
      --  Make an empty list;

      ensure
         count = 0

   copy (other: like Current)
      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

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

invariant
   empty_status: first_link = Void implies last_link = Void and upper = 0 and mem_idx = 0 and mem_lnk = Void;
   not_empty_status: first_link /= Void implies last_link /= Void and upper > 0 and mem_idx > 0 and mem_lnk /= Void;

end of TWO_WAY_LINKED_LIST[E]