Automatic generation produced by ISE Eiffel
indexing description: "[ Sequences of values, all of the same type or of a conforming one, accessible through integer indices in a contiguous interval. ]" status: "See notice at end of class" date: "$Date: 2001-11-16 20:32:23 +0000 (Fri, 16 Nov 2001) $" revision: "$Revision: 51435 $" class interface ARRAY [G] create make (min_index, max_index: INTEGER) -- Allocate array; set index interval to -- min_index .. max_index; set all values to default. -- (Make array empty if min_index = max_index + 1). require valid_bounds: min_index <= max_index + 1 ensure lower_set: lower = min_index upper_set: upper = max_index items_set: all_default make_from_array (a: ARRAY [G]) -- Initialize from the items of a. -- (Useful in proper descendants of class ARRAY, -- to initialize an array-like object from a manifest array.) require array_exists: a /= void feature -- Initialization make (min_index, max_index: INTEGER) -- Allocate array; set index interval to -- min_index .. max_index; set all values to default. -- (Make array empty if min_index = max_index + 1). require valid_bounds: min_index <= max_index + 1 ensure lower_set: lower = min_index upper_set: upper = max_index items_set: all_default make_from_array (a: ARRAY [G]) -- Initialize from the items of a. -- (Useful in proper descendants of class ARRAY, -- to initialize an array-like object from a manifest array.) require array_exists: a /= void feature -- Access area: SPECIAL [G] -- Special data zone -- (from TO_SPECIAL) entry (i: INTEGER): G -- Entry at index i, if in index interval require valid_key: valid_index (i) has (v: G): BOOLEAN -- Does v appear in array? -- (Reference or object equality, -- based on object_comparison.) ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty item (i: INTEGER): G -- Entry at index i, if in index interval -- Was declared in ARRAY as synonym of @. require -- from TABLE valid_key: valid_index (k) infix "@" (i: INTEGER): G -- Entry at index i, if in index interval -- Was declared in ARRAY as synonym of item. require -- from TABLE valid_key: valid_index (k) feature -- Measurement additional_space: INTEGER -- Proposed number of additional items -- (from RESIZABLE) ensure -- from RESIZABLE at_least_one: Result >= 1 capacity: INTEGER -- Number of available indices -- Was declared in ARRAY as synonym of count. ensure then consistent_with_bounds: Result = upper - lower + 1 count: INTEGER -- Number of available indices -- Was declared in ARRAY as synonym of capacity. ensure then consistent_with_bounds: Result = upper - lower + 1 Growth_percentage: INTEGER is 50 -- Percentage by which structure will grow automatically -- (from RESIZABLE) index_set: INTEGER_INTERVAL -- Range of acceptable indexes ensure -- from INDEXABLE not_void: Result /= void ensure then same_count: Result.count = count same_bounds: ((Result.lower = lower) and (Result.upper = upper)) lower: INTEGER -- Minimum index Minimal_increase: INTEGER is 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (v: G): INTEGER -- Number of times v appears in structure ensure -- from BAG non_negative_occurrences: Result >= 0 upper: INTEGER -- Maximum index feature -- Comparison is_equal (other: like Current): BOOLEAN -- Is array made of the same items as other? require -- from ANY other_not_void: other /= void ensure -- from ANY symmetric: Result implies other.is_equal (Current) consistent: standard_is_equal (other) implies Result feature -- Status report all_default: BOOLEAN -- Are all items set to default values? ensure definition: Result = (count = 0 or else ((item (upper) = void or else item (upper) = item (upper).default) and subarray (lower, upper - 1).all_default)) changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) extendible: BOOLEAN -- May items be added? -- (Answer: no, although array may be resized.) full: BOOLEAN -- Is structure filled to capacity? (Answer: yes) is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) is_inserted (v: G): BOOLEAN -- Has v been inserted by the most recent insertion? -- (By default, the value returned is equivalent to calling -- `has (v)'. However, descendants might be able to provide more -- efficient implementations.) -- (from COLLECTION) object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? (Answer: no.) resizable: BOOLEAN -- May capacity be changed? (Answer: yes.) -- (from RESIZABLE) same_items (other: like Current): BOOLEAN -- Do other and Current have same items? require other_not_void: other /= void ensure definition: Result = ((count = other.count) and then (count = 0 or else (item (upper) = other.item (other.upper) and subarray (lower, upper - 1).same_items (other.subarray (other.lower, other.upper - 1))))) valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the array? ensure then -- from INDEXABLE only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper)) valid_index_set: BOOLEAN feature -- Status setting compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison feature -- Element change enter (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require valid_key: valid_index (i) fill (other: CONTAINER [G]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from COLLECTION) require -- from COLLECTION other_not_void: other /= void extendible force (v: like item; i: INTEGER) -- Assign item v to i-th entry. -- Always applicable: resize the array if i falls out of -- currently defined bounds; preserve existing items. ensure inserted: item (i) = v higher_count: count >= old count put (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require -- from TABLE valid_key: valid_index (k) ensure then -- from INDEXABLE insertion_done: item (k) = v subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER) -- Copy items of other within bounds start_pos and end_pos -- to current array starting at index index_pos. require other_not_void: other /= void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) enough_space: (upper - index_pos) >= (end_pos - start_pos) feature -- Removal clear_all -- Reset all items to default values. ensure stable_lower: lower = old lower stable_upper: upper = old upper default_items: all_default discard_items -- Reset all items to default values with reallocation. ensure default_items: all_default prune_all (v: G) -- Remove all occurrences of v. -- (Reference or object equality, -- based on object_comparison.) -- (from COLLECTION) require -- from COLLECTION prunable ensure -- from COLLECTION no_more_occurrences: not has (v) feature -- Resizing automatic_grow -- Change the capacity to accommodate at least -- Growth_percentage more items. -- (from RESIZABLE) ensure -- from RESIZABLE increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100 grow (i: INTEGER) -- Change the capacity to at least i. ensure -- from RESIZABLE new_capacity: capacity >= i resize (min_index, max_index: INTEGER) -- Rearrange array so that it can accommodate -- indices down to min_index and up to max_index. -- Do not lose any previously entered item. require good_indices: min_index <= max_index ensure no_low_lost: lower = min_index or else lower = old lower no_high_lost: upper = max_index or else upper = old upper feature -- Conversion linear_representation: LINEAR [G] -- Representation as a linear structure to_c: ANY -- Address of actual sequence of values, -- for passing to external (non-Eiffel) routines. feature -- Duplication copy (other: like Current) -- Reinitialize by copying all the items of other. -- (This is also used by clone.) require -- from ANY other_not_void: other /= void type_identity: same_type (other) ensure -- from ANY is_equal: is_equal (other) ensure then equal_areas: area.is_equal (other.area) subarray (start_pos, end_pos: INTEGER): like Current -- Array made of items of current array within -- bounds start_pos and end_pos. require valid_start_pos: valid_index (start_pos) valid_end_pos: valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) ensure lower: Result.lower = start_pos upper: Result.upper = end_pos invariant area_exists: area /= void consistent_size: capacity = upper - lower + 1 non_negative_count: count >= 0 index_set_has_same_count: valid_index_set index_set_has_same_bounds: ((index_set.lower = lower) and (index_set.upper = lower + count - 1)) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from RESIZABLE increase_by_at_least_one: minimal_increase >= 1 -- from BOUNDED valid_count: count <= capacity full_definition: full = (count = capacity) -- from FINITE empty_definition: is_empty = (count = 0) non_negative_count: count >= 0 -- from INDEXABLE index_set_not_void: index_set /= void indexing library: "[ EiffelBase: Library of reusable components for Eiffel. ]" status: "[ Copyright 1986-2001 Interactive Software Engineering (ISE). For ISE customers the original versions are an ISE product covered by the ISE Eiffel license and support agreements. ]" license: "[ EiffelBase may now be used by anyone as FREE SOFTWARE to develop any product, public-domain or commercial, without payment to ISE, under the terms of the ISE Free Eiffel Library License (IFELL) at http://eiffel.com/products/base/license.html. ]" source: "[ Interactive Software Engineering Inc. ISE Building 360 Storke Road, Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Electronic mail <info@eiffel.com> Customer support http://support.eiffel.com ]" info: "[ For latest info see award-winning pages: http://eiffel.com ]" end -- class ARRAY -- Generated by ISE Eiffel --
For more details: www.eiffel.com