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

creation
   make (minindex, maxindex: INTEGER)
      --  Make array with range [minindex .. maxindex]. 
      --  When maxindex = minindex - 1, the array is empty.

      require
         minindex - 1 <= maxindex
      ensure
         lower = minindex;
         upper = maxindex;
         all_cleared

   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
         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 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
         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: like item; index: INTEGER)
      --  Put element at position index. Current is
      --  resized if index is not inside current bounds.
      --  New bounds are initialized with default values.

      require
         true
      require else
         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
         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 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 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
         capacity = old capacity;
         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.

      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 :

   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 ARRAYED_COLLECTION
   capacity: INTEGER
      --  Internal storage capacity in number of item.


feature(s) from ARRAYED_COLLECTION
   sub_array (low, up: INTEGER): like Current
      require
         valid_index(low);
         valid_index(up);
         low <= up
      ensure
         Result.lower = low;
         same_type(Result);
         Result.count = up - low + 1;
         Result.lower = low 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 empty
      ensure
         Result.is_not_null

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

   make (minindex, maxindex: INTEGER)
      --  Make array with range [minindex .. maxindex]. 
      --  When maxindex = minindex - 1, the array is empty.

      require
         minindex - 1 <= maxindex
      ensure
         lower = minindex;
         upper = maxindex;
         all_cleared

   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
         empty;
         needed_capacity <= capacity;
         lower = low

feature(s) from ARRAY
   --  Modification :

   resize (minindex, maxindex: INTEGER)
      --  Resize the array. No elements will be lost in the 
      --  intersection of [old lower .. old upper] and 
      --  [minindex .. maxindex].
      --  New positions are initialized with appropriate 
      --  default values.

      require
         minindex - 1 <= maxindex

feature(s) from ARRAY
   --  Implementation of deferred :

   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
   capacity >= upper - lower + 1;
   capacity > 0 implies storage.is_not_null;

end of ARRAY[E]