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]