class interface KL_FIXED_ARRAY_ROUTINES[G]

feature(s) from KL_IMPORTED_FIXED_ARRAY_TYPE
   --  Type anchors

   FIXED_ARRAY_TYPE: FIXED_ARRAY[G]

feature(s) from KL_FIXED_ARRAY_ROUTINES
   --  Initialization

   make (n: INTEGER): like FIXED_ARRAY_TYPE
      --  Create a new fixed array being able to contain n items.

      require
         non_negative_n: n >= 0
      ensure
         fixed_array_not_void: Result /= Void;
         valid_fixed_array: valid_fixed_array(Result);
         count_set: Result.count = n

   make_from_array (an_array: ARRAY[G]): like FIXED_ARRAY_TYPE
      --  Create a new fixed array with items from an_array.

      require
         an_array_not_void: an_array /= Void
      ensure
         fixed_array_not_void: Result /= Void;
         valid_fixed_array: valid_fixed_array(Result);
         count_set: Result.count = an_array.count -- 			same_items: forall i in 0.. (Result.count - 1),
 -- 				Result.item (i) = an_array.item (an_array.lower + i)

feature(s) from KL_FIXED_ARRAY_ROUTINES
   --  Conversion

   to_fixed_array (an_array: ARRAY[G]): like FIXED_ARRAY_TYPE
      --  Fixed array filled with items from an_array.
      --  The fixed array and an_array may share internal
      --  data. Use make_from_array if this is a concern.

      require
         an_array_not_void: an_array /= Void
      ensure
         fixed_array_not_void: Result /= Void;
         valid_fixed_array: valid_fixed_array(Result);
         count_set: Result.count >= an_array.count -- 			same_items: forall i in 0.. (an_array.count - 1),
 -- 				Result.item (i) = an_array.item (an_array.lower + i)

feature(s) from KL_FIXED_ARRAY_ROUTINES
   --  Status report

   has (an_array: like FIXED_ARRAY_TYPE; v: G): BOOLEAN
      --  Does v appear in an_array?

      require
         an_array_not_void: an_array /= Void

   valid_fixed_array (an_array: like FIXED_ARRAY_TYPE): BOOLEAN
      --  Make sure that the lower bound of an_array is zero.

      require
         an_array_not_void: an_array /= Void

feature(s) from KL_FIXED_ARRAY_ROUTINES
   --  Resizing

   resize (an_array: like FIXED_ARRAY_TYPE; n: INTEGER): like FIXED_ARRAY_TYPE
      --  Resize an_array so that it contains n items.
      --  Do not lose any previously entered items.
      --  Note: the returned fixed array  might be an_array
      --  or a newly created fixed array where items from
      --  an_array have been copied to.

      require
         an_array_not_void: an_array /= Void;
         valid_fixed_array: valid_fixed_array(an_array);
         n_large_enough: n >= an_array.count
      ensure
         fixed_array_not_void: Result /= Void;
         valid_fixed_array: valid_fixed_array(Result);
         count_set: Result.count = n

feature(s) from KL_FIXED_ARRAY_ROUTINES
   --  Removal

   clear_all (an_array: like FIXED_ARRAY_TYPE)
      --  Reset all items to default values.

      require
         an_array_not_void: an_array /= Void;
         valid_fixed_array: valid_fixed_array(an_array)


end of KL_FIXED_ARRAY_ROUTINES[G]