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]