class interface ARRAY[E]
   --
   -- General purpose resizable ARRAYs.
   --

creation
   make (min_index, max_index: INTEGER)
      -- Prepare the array to hold values for indexes in range
      -- [min_index .. max_index]. Set all values to default.
      -- When max_index = min_index - 1, the array is_empty.

      require
         valid_bounds: min_index <= max_index + 1
      ensure
         lower_set: lower = min_index;
         upper_set: upper = max_index;
         items_set: all_default

   with_capacity (needed_capacity, low: INTEGER)
      -- Create an empty array with capacity initialized
      -- at least to needed_capacity and lower set to low.

      require
         needed_capacity >= 0
      ensure
         is_empty;
         needed_capacity <= capacity;
         lower = low

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

      require
         model /= Void
      ensure
         lower = model.lower;
         upper = model.upper;
         count = model.count

feature(s) from COLLECTION
   -- Indexing:

   lower: INTEGER
      -- Lower index bound.


   upper: INTEGER
      -- 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 (i: INTEGER): E
      -- Item at the corresponding index i.

      require
         valid_index(i)

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

      require
         valid_index(i)

   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; i: INTEGER)
      -- Make element the item at index i.

      require
         valid_index(i)
      ensure
         item(i) = 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
         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: like item; index: INTEGER)
      -- Make element the item at index, enlarging the collection if
      -- necessary (new bounds except index are initialized with
      -- default values).

      require
         True
      require else
         index >= lower
      ensure
         lower = index.min(old lower);
         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
         lower = model.lower;
         upper = model.upper;
         count = model.count

feature(s) from COLLECTION
   -- Removing:

   remove_first
      -- Remove the first element of the collection.

      require
         not is_empty
      ensure
         upper = old upper;
         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
         capacity = old capacity;
         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 (element: 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(element,item(Result))

   fast_index_of (element: 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 element = 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 (min, max: 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 <= min;
         max <= upper;
         min <= max + 1
      ensure
         same_dynamic_type(Result);
         Result.count = max - min + 1;
         Result.lower = lower

   reverse
      -- Reverse the order of the elements.

      ensure
         count = old count

feature(s) from ARRAYED_COLLECTION   capacity: INTEGER
      -- Internal storage capacity in number of item.


   subarray (min, max: INTEGER): like Current
      -- New collection consisting of items at indexes in [min .. max].
      -- Result has the same dynamic type as Current.
      -- See also slice.

      require
         lower <= min;
         max <= upper;
         min <= max + 1
      ensure
         Result.lower = min;
         same_dynamic_type(Result);
         Result.count = max - min + 1;
         Result.lower = min or Result.lower = 0

feature(s) from ARRAYED_COLLECTION
   -- Interfacing with C:

   to_external: POINTER
      -- Gives C access into the internal storage of the ARRAY.
      -- Result is pointing the element at index lower.
      --
      -- NOTE: do not free/realloc the Result. Resizing of the array
      --       can makes this pointer invalid.

      require
         not is_empty
      ensure
         Result.is_not_null

feature(s) from ARRAY
   -- Creation and Modification:

   make (min_index, max_index: INTEGER)
      -- Prepare the array to hold values for indexes in range
      -- [min_index .. max_index]. Set all values to default.
      -- When max_index = min_index - 1, the array is_empty.

      require
         valid_bounds: min_index <= max_index + 1
      ensure
         lower_set: lower = min_index;
         upper_set: upper = max_index;
         items_set: all_default

   with_capacity (needed_capacity, low: INTEGER)
      -- Create an empty array with capacity initialized
      -- at least to needed_capacity and lower set to low.

      require
         needed_capacity >= 0
      ensure
         is_empty;
         needed_capacity <= capacity;
         lower = low

feature(s) from ARRAY
   -- Modification:

   resize (min_index, max_index: INTEGER)
      -- Resize to bounds min_index and max_index. Do not lose any
      -- item whose index is in both [lower .. upper] and
      -- [min_index .. max_index]. New positions if any are
      -- initialized with the appropriate default value.

      require
         min_index <= max_index + 1
      ensure
         lower = min_index;
         upper = max_index

   reindex (new_lower: INTEGER)
      -- Change indexing to take in account the expected new_lower
      -- index. The upper index is translated accordingly.

      ensure
         lower = new_lower;
         count = old count


invariant
   valid_bounds: lower <= upper + 1;
   capacity >= upper - lower + 1;
   capacity > 0 implies storage.is_not_null;

end of ARRAY[E]