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 available indices.

      ensure
         Result = upper - lower + 1

   is_empty: BOOLEAN
      -- Is collection empty ?

      ensure
         Result = (count = 0)

feature(s) from COLLECTION
   -- Accessing:

   item (index: INTEGER): E
      -- Item at the corresponding index i.

      require
         valid_index(index)

   infix "@" (index: INTEGER): E
      -- Item at the corresponding index i.

      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
         not is_empty
      ensure
         Result = item(upper)

feature(s) from COLLECTION
   -- Writing:

   put (element: like item; index: INTEGER)
      -- Make element the item at index i.

      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 every item to its default value.
      -- The count is not affected (see also clear).

      ensure
         stable_upper: upper = old upper;
         stable_lower: lower = old lower;
         all_default

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
         index.in_range(lower,upper + 1)
      ensure
         item(index) = element;
         count = 1 + old count;
         upper = 1 + old upper

   append_collection (other: COLLECTION[E])
      -- Append other to Current.

      require
         other /= Void
      ensure
         count = other.count + old count

feature(s) from COLLECTION
   -- Modification:

   force (element: E; index: INTEGER)
      -- Make element the item at index, enlarging the collection if
      -- necessary (new bounds except index are initialized with
      -- default values).

      require
         index >= lower
      ensure
         upper = index.max(old upper);
         item(index) = element

   copy (other: like Current)
      -- Reinitialize by copying all the items of other.

      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

   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 is_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 is_empty
      ensure
         count = old count - 1;
         upper = old upper - 1

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

      ensure
         upper = 0;
         is_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.
      --
      -- Note: we'll have to mimic what's done in the new ELKS STRING class
      -- for index_of (ie. to add an extra argument). This is in the todo
      -- list ... let people switch first to ELKS 2001 at time being.

      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:

   is_equal (other: like Current): BOOLEAN
      -- Do both collections have the same lower, upper, and
      -- items?
      -- The basic = is used for comparison of items.
      -- See also is_equal_map.

      require
         other /= Void
      ensure
         Result implies lower = other.lower and upper = other.upper;
         generating_type = other.generating_type implies Result = other.is_equal(Current)

   is_equal_map (other: like Current): BOOLEAN
      -- Do both collections have the same lower, upper, and
      -- items?
      -- Feature is_equal is used for comparison of items.
      -- See also is_equal.

      ensure
         Result implies lower = other.lower and upper = other.upper

   all_default: BOOLEAN
      -- Do all items have their type's default value?
      -- Note: for non Void items, the test is performed with the 
      -- is_default predicate.


   same_items (other: COLLECTION[E]): BOOLEAN
      -- Do both collections have the same items? The basic = is used
      -- for comparison of items and indices are not considered (for
      -- example this routine may yeld True with Current indexed in
      -- range [1..2] and other indexed in range [2..3]).

      require
         other /= Void
      ensure
         Result implies count = other.count

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

      ensure
         Result >= 0

   fast_occurrences (element: like item): INTEGER
      -- Number of occurrences of element using basic = for comparison.
      -- Also consider occurrences 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
   -- Agents based features:

   do_all (action: PROCEDURE[ANY,TUPLE[ANY]])
      -- Apply action to every item of Current.


   for_all (test: PREDICATE[ANY,TUPLE[ANY]]): BOOLEAN
      -- Do all items satisfy test?


   exists (test: PREDICATE[ANY,TUPLE[ANY]]): BOOLEAN
      -- Does at least one item satisfy test?


feature(s) from COLLECTION
   -- Other features:

   get_new_iterator: ITERATOR[E]

   replace_all (old_value, new_value: like item)
      -- Replace all occurrences 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;
         occurrences(old_value) = 0

   fast_replace_all (old_value, new_value: like item)
      -- Replace all occurrences 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_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
      -- New collection consisting of items at indexes in [min..max].
      -- Result has the same dynamic type as Current.
      -- The lower index of the Result is the same as lower.

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

   reverse
      -- Reverse the order of the elements.

      ensure
         count = old count

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

      ensure
         count = 0


invariant
   valid_bounds: lower <= upper + 1;
   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]