class interface ARRAY2[E]
   -- 
   --  General prurpose, resizable, two dimensional array.
   -- 

creation
   make (line_min, line_max, column_min, column_max: INTEGER)
      --  Reset all bounds line_minimum / line_maximum / column_minimum and
      --  column_maximum using arguments as new values.
      --  All elements are set to the default value of type E.

      require
         line_min <= line_max;
         column_min <= column_max
      ensure
         line_minimum = line_min;
         line_maximum = line_max;
         column_minimum = column_min;
         column_maximum = column_max

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

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

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

   from_collection (contents: COLLECTION[E]; line_min, line_max, column_min, column_max: INTEGER)
      --   Reset all bounds using line_min, line_max, column_min,
      --   and column_max .
      --   Copy all elements of contents, line by line into Current.

      require
         line_min <= line_max;
         column_min <= column_max;
         contents.count = (line_max - line_min + 1) * column_max - column_min + 1
      ensure
         line_minimum = line_min;
         line_maximum = line_max;
         column_minimum = column_min;
         column_maximum = column_max;
         count = contents.count

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

      require
         model /= Void
      ensure
         line_minimum = model.lower;
         line_maximum = model.upper;
         column_minimum = model.first.lower;
         column_maximum = model.first.upper;
         count1 = model.count;
         count2 > 0 implies count2 = model.first.count

   array2 (model: ARRAY[ARRAY[E]])

feature(s) from COLLECTION2
   --  Indexing :

   lower1: INTEGER
      --  Upper index bounds.


feature(s) from COLLECTION2
   --  Indexing :

   lower2: INTEGER
      --  Upper index bounds.


   line_minimum: INTEGER
      --  Equivalent of lower1.


   column_minimum: INTEGER
      --  Equivalent of lower2.


   upper1: INTEGER
      --  Upper index bounds.


   upper2: INTEGER
      --  Upper index bounds.


   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 (element: like item; line, column: INTEGER)
      require
         valid_index(line,column)
      ensure
         item(line,column) = element

   force (x: 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
         true
      require else
         line >= 0;
         column >= 0
      ensure
         item(line,column) = x;
         count >= old count

feature(s) from COLLECTION2
   --  Index validity :

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

feature(s) from COLLECTION2
   --  Index validity :

   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_index2(column))

feature(s) from COLLECTION2
   --  Counting :

   count1: INTEGER
      --  Size of the first dimension.

      ensure
         Result = upper1 - lower1 + 1

   line_count: INTEGER
      --  Equivalent of count1.


   count2: INTEGER
      --  Size of the second dimension.

      ensure
         Result = upper2 - lower2 + 1

   column_count: INTEGER

   count: INTEGER
      --  Total number of elements.

      ensure
         Result = line_count * column_count

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 (element: E)
      --  Set all item with value v.

      ensure
         count = old count

   clear_all
      --  Set all items to default values.

      ensure
         count = old count

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

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

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

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

      require
         model /= Void
      ensure
         line_minimum = model.lower;
         line_maximum = model.upper;
         column_minimum = model.first.lower;
         column_maximum = model.first.upper;
         count1 = model.count;
         count2 > 0 implies count2 = model.first.count

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

   all_cleared: BOOLEAN
      --  Are all items set to default values ?


   same_as (other: COLLECTION2[E]): BOOLEAN
      --  Unlike is_equal, this feature can be used to compare
      --  distinct implementation of COLLECTION2.

      require
         other /= Void
      ensure
         Result implies standard_same_as(other)

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 :

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

      ensure
         Result >= 0;
         Result >= 0

   fast_nb_occurrences (elt: E): INTEGER
      --  Number of occurrences using =.

      ensure
         Result >= 0;
         Result >= 0

   has (x: like item): BOOLEAN
      --  Search if a element x is in the array using equal.
      --  See also fast_has to chose the apropriate one.


   fast_has (x: like item): BOOLEAN
      --   Search if a element x is in the array using =.


   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

   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,line_max);
         valid_index(column_min,column_max)
      require else
         valid_index(line_min,column_min);
         valid_index(line_min,column_min)
      ensure
         Result.lower1 = line_min;
         Result.lower2 = column_min;
         Result.upper1 = line_max;
         Result.upper2 = column_max;
         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,line_max);
         valid_index(column_min,column_max)
      ensure
         count = old count

feature(s) from ARRAY2
   --  Creation / modification :

   make (line_min, line_max, column_min, column_max: INTEGER)
      --  Reset all bounds line_minimum / line_maximum / column_minimum and
      --  column_maximum using arguments as new values.
      --  All elements are set to the default value of type E.

      require
         line_min <= line_max;
         column_min <= column_max
      ensure
         line_minimum = line_min;
         line_maximum = line_max;
         column_minimum = column_min;
         column_maximum = column_max

   from_collection (contents: COLLECTION[E]; line_min, line_max, column_min, column_max: INTEGER)
      --   Reset all bounds using line_min, line_max, column_min,
      --   and column_max .
      --   Copy all elements of contents, line by line into Current.

      require
         line_min <= line_max;
         column_min <= column_max;
         contents.count = (line_max - line_min + 1) * column_max - column_min + 1
      ensure
         line_minimum = line_min;
         line_maximum = line_max;
         column_minimum = column_min;
         column_maximum = column_max;
         count = contents.count

feature(s) from ARRAY2
   --  Resizing :

   resize (line_min, line_max, column_min, column_max: INTEGER)
      --  Resize bounds of the Current array

      require
         line_max >= line_min;
         column_max >= column_min
      ensure
         line_minimum = line_min;
         line_maximum = line_max;
         column_minimum = column_min;
         column_maximum = column_max

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

   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)

feature(s) from ARRAY2
   --  Only for ARRAY2 :

   transpose
      --  Transpose the Current array

      ensure
         line_minimum = old column_minimum;
         column_minimum = old line_minimum;
         line_maximum = old column_maximum;
         column_maximum = old line_maximum;
         count = old count

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


invariant
   count2 = upper2 - lower2 + 1;
   capacity >= count;

end of ARRAY2[E]