class interface FIXED_ARRAY2[E]
   --
   -- Resizable two dimensional array.
   -- Unlike ARRAY2, the lower1 bound and the lower2 bound are
   -- frozen to 0. Thus, one can expect better performances.
   --

creation
   make (new_count1, new_count2: INTEGER)
      -- Create or reset Current with new dimensions.
      -- All elements are set to the default value of type E.

      require
         new_count1 > 0;
         new_count2 > 0
      ensure
         count1 = new_count1;
         count2 = new_count2;
         all_default

   copy (other: like Current)
      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

   from_collection2 (model: COLLECTION2[like item])
      --  Uses model to initialize Current.

      require
         model /= Void
      ensure
         count1 = model.count1;
         count2 = model.count2

   from_collection (model: COLLECTION2[like item])
      -- Uses the model to update Current.


   from_model (model: COLLECTION[COLLECTION[E]])
      -- The model is used to fill line by line Current.
      -- Assume all sub-collections of model have the same
      -- number of lines.

      require
         model /= Void
      ensure
         count1 = model.count;
         count2 > 0 implies count2 = model.first.count

feature(s) from COLLECTION2
   -- Indexing:

   lower1: INTEGER
      -- Lower index bounds.


   lower2: INTEGER
      -- Lower index bounds.


   line_minimum: INTEGER
      -- Equivalent of lower1.


   column_minimum: INTEGER
      -- Equivalent of lower2.


   upper1: INTEGER
      -- Total number of elements.


   upper2: INTEGER
      -- Total number of elements.


   line_maximum: INTEGER
      -- Equivalent of upper1.


   column_maximum: INTEGER
      -- Equivalent of upper2.


feature(s) from COLLECTION2
   -- Reading:

   item (line, column: INTEGER): E
      require
         valid_index(line,column)

feature(s) from COLLECTION2
   -- Writing:

   put (x: like item; line, column: INTEGER)
      require
         valid_index(line,column)
      ensure
         item(line,column) = x

   force (element: like item; line, column: INTEGER)
      -- Put element at position (line,column). Collection is
      -- resized first when (line,column) is not inside current
      -- bounds. New bounds are initialized with default values.

      require
         line >= 0;
         column >= 0
      ensure
         item(line,column) = element;
         count >= old count

feature(s) from COLLECTION2
   -- Index validity:

   valid_line (line: INTEGER): BOOLEAN
      ensure
         Result = (lower1 <= line and line <= upper1)

   valid_index1 (line: INTEGER): BOOLEAN
      ensure
         Result = (lower1 <= line and line <= upper1)

   valid_column (column: INTEGER): BOOLEAN
      ensure
         Result = (lower2 <= column and column <= upper2)

   valid_index2 (column: INTEGER): BOOLEAN
      ensure
         Result = (lower2 <= column and column <= upper2)

   valid_index (line, column: INTEGER): BOOLEAN
      ensure
         Result = (valid_line(line) and valid_column(column))

feature(s) from COLLECTION2
   -- Counting:

   count1: INTEGER
      -- Total number of elements.


   line_count: INTEGER
      -- Equivalent of count1.


   count2: INTEGER
      -- Total number of elements.


   column_count: INTEGER

   count: INTEGER
      -- Total number of elements.


feature(s) from COLLECTION2   swap (line1, column1, line2, column2: INTEGER)
      -- Swap the element at index (line1,column1) with the
      -- the element at index (line2,column2).

      require
         valid_index(line1,column1);
         valid_index(line2,column2)
      ensure
         item(line1,column1) = old item(line2,column2);
         item(line2,column2) = old item(line1,column1);
         count = old count

   set_all_with (x: E)
      --  All element are set with the value x.

      ensure
         count = old count

   clear_all
      -- Set all items to default values.

      ensure
         count = old count;
         all_default

feature(s) from COLLECTION2
   -- Creating or initializing:

   from_collection2 (model: COLLECTION2[like item])
      --  Uses model to initialize Current.

      require
         model /= Void
      ensure
         count1 = model.count1;
         count2 = model.count2

   from_model (model: COLLECTION[COLLECTION[E]])
      -- The model is used to fill line by line Current.
      -- Assume all sub-collections of model have the same
      -- number of lines.

      require
         model /= Void
      ensure
         count1 = model.count;
         count2 > 0 implies count2 = model.first.count

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

   all_default: BOOLEAN
      -- Do all items have their type's default value?


feature(s) from COLLECTION2
   -- 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 COLLECTION2
   -- Miscellaneous features:

   occurrences (elt: E): INTEGER
      -- Number of occurrences using equal.
      -- See also fast_occurrences to chose the apropriate one.

      ensure
         Result >= 0

   fast_occurrences (elt: E): INTEGER
      -- Number of occurrences using =.
      -- See also occurrences to chose the apropriate one.

      ensure
         Result >= 0

   has (x: like item): BOOLEAN
      -- Look for x using equal for comparison.


   fast_has (x: like item): BOOLEAN
      -- Same as has but use = for comparison


   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

   sub_collection2 (line_min, line_max, column_min, column_max: INTEGER): like Current
      -- Create a new object using selected area of Current.

      require
         valid_index(line_min,column_min);
         valid_index(line_max,column_max)
      ensure
         Result /= Void

   set_area (element: like item; line_min, line_max, column_min, column_max: INTEGER)
      -- Set all the elements of the selected area rectangle with element.

      require
         valid_index(line_min,column_min);
         valid_index(line_max,column_max)
      ensure
         count = old count

feature(s) from FIXED_ARRAY2   make (new_count1, new_count2: INTEGER)
      -- Create or reset Current with new dimensions.
      -- All elements are set to the default value of type E.

      require
         new_count1 > 0;
         new_count2 > 0
      ensure
         count1 = new_count1;
         count2 = new_count2;
         all_default

   from_collection (model: COLLECTION2[like item])
      -- Uses the model to update Current.


feature(s) from FIXED_ARRAY2
   -- Implementation of others feature from COLLECTION2:

   copy (other: like Current)
      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

   is_equal (other: like Current): BOOLEAN
      require
         other /= Void
      ensure
         generating_type = other.generating_type implies Result = other.is_equal(Current)

feature(s) from FIXED_ARRAY2
   -- Writing:

   slice (l1, up1, l2, up2: INTEGER): like Current
      -- Create a new collection initialized with elements of
      -- range low..up. Result has the same dynamic type
      -- as Current collection.


   set_slice (element: like item; l1, up1, l2, up2: INTEGER)
      -- Set all the elements in the
      -- range [(l1,up1),(l2,up2)] of
      -- Current with the element 'element'.


feature(s) from FIXED_ARRAY2
   -- Resizing:

   resize (new_count1, new_count2: INTEGER)
      require
         new_count1 > 0;
         new_count2 > 0
      ensure
         upper1 = new_count1 - 1;
         count1 = new_count1;
         upper2 = new_count2 - 1;
         count2 = new_count2;
         count = new_count1 * new_count2

feature(s) from FIXED_ARRAY2
   -- Other features:

   transpose
      -- Transpose the Current array


   to_external: POINTER
      -- Gives C access to the internal storage (may be dangerous).



invariant
   count1 = upper1 + 1;
   count2 = upper2 + 1;
   count = count1 * count2;
   capacity >= count;

end of FIXED_ARRAY2[E]