class interface KL_ARRAY_ROUTINES[G]

feature(s) from KL_ARRAY_ROUTINES
   --  Initialization

   make_from_array (an_array: ARRAY[G]; min_index: INTEGER): ARRAY[G]
      --  Create a new array and initialize it
      --  with items from an_array.

      require
         an_array_not_void: an_array /= Void
      ensure
         array_not_void: Result /= Void;
         lower_set: Result.lower = min_index;
         count_set: Result.count = an_array.count -- 			same_items: forall i in Result.lower .. Result.upper,
 -- 				Result.item (i) = an_array.item (i + an_array.lower - min_index)

feature(s) from KL_ARRAY_ROUTINES
   --  Status report

   has (an_array: ARRAY[G]; v: G): BOOLEAN
      --  Does v appear in an_array?

      require
         an_array_not_void: an_array /= Void

feature(s) from KL_ARRAY_ROUTINES
   --  Access

   subarray (an_array: ARRAY[G]; start_pos, end_pos, min_index: INTEGER): ARRAY[G]
      --  Array made up of items from an_array within
      --  bounds start_pos and end_pos

      require
         an_array_not_void: an_array /= Void;
         start_pos_large_enough: start_pos >= an_array.lower;
         end_pos_small_enough: end_pos <= an_array.upper;
         valid_bounds: start_pos <= end_pos + 1
      ensure
         array_not_void: Result /= Void;
         lower_set: Result.lower = min_index;
         count_set: Result.count = end_pos - start_pos + 1 -- 			same_items: forall i in Result.lower .. Result.upper,
 -- 				Result.item (i) = an_array.item (i + start_pos - min_index)

feature(s) from KL_ARRAY_ROUTINES
   --  Element change

   subcopy (an_array, other: ARRAY[G]; start_pos, end_pos, index_pos: INTEGER)
      --  Copy items of other within bounds start_pos and end_pos
      --  to an_array starting at index index_pos.

      require
         an_array_not_void: an_array /= Void;
         other_not_void: other /= Void;
         not_same: an_array /= other;
         start_pos_large_enough: start_pos >= other.lower;
         end_pos_small_enough: end_pos <= other.upper;
         valid_bounds: start_pos <= end_pos + 1;
         index_pos_large_enough: index_pos >= an_array.lower;
         enough_space: an_array.upper - index_pos >= end_pos - start_pos

feature(s) from KL_ARRAY_ROUTINES
   --  Removal

   clear_all (an_array: ARRAY[G])
      --  Reset all items to default values.

      require
         an_array_not_void: an_array /= Void


end of KL_ARRAY_ROUTINES[G]