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]