note description: "Contiguous integer intervals" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2019-07-05 15:26:16 +0000 (Fri, 05 Jul 2019) $" revision: "$Revision: 103325 $" class interface INTEGER_INTERVAL create make feature -- Initialization adapt (other: INTEGER_INTERVAL) -- Reset to be the same interval as other. require other_not_void: other /= Void ensure same_lower: lower = other.lower same_upper: upper = other.upper same_lower_defined: Lower_defined = other.Lower_defined same_upper_defined: Upper_defined = other.Upper_defined feature -- Access Lower_defined: BOOLEAN = True -- Is there a lower bound? lower: INTEGER_32 -- Smallest value in interval. Upper_defined: BOOLEAN = True -- Is there an upper bound? upper: INTEGER_32 -- Largest value in interval. item alias "[]" (i: INTEGER_32): INTEGER_32 -- Entry at index i, if in index interval -- Was declared in INTEGER_INTERVAL as synonym of at. at alias "@" (i: INTEGER_32): INTEGER_32 -- Entry at index i, if in index interval -- Was declared in INTEGER_INTERVAL as synonym of item. has alias "∋" (v: INTEGER_32): BOOLEAN -- Does v appear in interval? -- Was declared in INTEGER_INTERVAL as synonym of valid_index. ensure then iff_within_bounds: Result = ((Upper_defined implies v <= upper) and (Lower_defined implies v >= lower)) valid_index (v: INTEGER_32): BOOLEAN -- Does v appear in interval? -- Was declared in INTEGER_INTERVAL as synonym of has. ensure then iff_within_bounds: Result = ((Upper_defined implies v <= upper) and (Lower_defined implies v >= lower)) feature -- Measurement occurrences (v: INTEGER_32): INTEGER_32 -- Number of times v appears in structure ensure then one_iff_in_bounds: Result = 1 implies has (v) zero_otherwise: Result /= 1 implies Result = 0 capacity: INTEGER_32 -- Maximum number of items in interval -- (here the same thing as count) count: INTEGER_32 -- Number of items in interval ensure then definition: Result = upper - lower + 1 index_set: INTEGER_INTERVAL -- Range of acceptable indexes. -- (here: the interval itself) ensure then index_set_is_range: Result ~ Current feature -- Comparison is_equal (other: like Current): BOOLEAN -- Is array made of the same items as other? ensure then iff_same_bounds: Result = ((Lower_defined implies (other.Lower_defined and lower = other.lower)) and (Upper_defined implies (other.Upper_defined and upper = other.upper))) feature -- Status report all_cleared: BOOLEAN -- Are all items set to default values? ensure then iff_at_zero: Result = ((lower = 0) and (upper = 0)) extendible: BOOLEAN -- May new items be added? -- Answer: yes prunable: BOOLEAN -- May individual items be removed? -- Answer: no feature -- Element change extend (v: INTEGER_32) -- Make sure that interval goes all the way -- to v (up or down). -- Was declared in INTEGER_INTERVAL as synonym of put. ensure then extended_down: lower = (old lower).min (v) extended_up: upper = (old upper).max (v) put (v: INTEGER_32) -- Make sure that interval goes all the way -- to v (up or down). -- Was declared in INTEGER_INTERVAL as synonym of extend. ensure then extended_down: lower = (old lower).min (v) extended_up: upper = (old upper).max (v) feature -- Resizing resize (min_index, max_index: INTEGER_32) -- Rearrange interval to go from at most -- min_index to at least max_index, -- encompassing previous bounds. resize_exactly (min_index, max_index: INTEGER_32) -- Rearrange interval to go from -- min_index to max_index. grow (i: INTEGER_32) -- Ensure that capacity is at least i. ensure then no_loss_from_bottom: lower <= old lower no_loss_from_top: upper >= old upper trim -- Decrease capacity to the minimum value. -- Apply to reduce allocated storage. feature -- Removal wipe_out -- Remove all items. feature -- Conversion as_array: ARRAY [INTEGER_32] -- Plain array containing interval's items require finite: Upper_defined and Lower_defined ensure same_lower: Result.lower = lower same_upper: Result.upper = upper linear_representation: LINEAR [INTEGER_32] -- Representation as a linear structure feature -- Duplication copy (other: like Current) -- Reset to be the same interval as other. subinterval (start_pos, end_pos: INTEGER_32): like Current -- Interval made of items of current array within -- bounds start_pos and end_pos. feature -- Iteration do_all (action: PROCEDURE [INTEGER_32]) -- Apply action to every item of current interval. require action_exists: action /= Void finite: Upper_defined and Lower_defined for_all (condition: FUNCTION [INTEGER_32, BOOLEAN]): BOOLEAN -- Do all interval's values satisfy condition? require finite: Upper_defined and Lower_defined condition_not_void: condition /= Void ensure consistent_with_count: Result = (hold_count (condition) = count) exists (condition: FUNCTION [INTEGER_32, BOOLEAN]): BOOLEAN -- Does at least one of interval's values -- satisfy condition? require finite: Upper_defined and Lower_defined condition_not_void: condition /= Void ensure consistent_with_count: Result = (hold_count (condition) > 0) exists1 (condition: FUNCTION [INTEGER_32, BOOLEAN]): BOOLEAN -- Does exactly one of interval's values -- satisfy condition? require finite: Upper_defined and Lower_defined condition_not_void: condition /= Void ensure consistent_with_count: Result = (hold_count (condition) = 1) hold_count (condition: FUNCTION [INTEGER_32, BOOLEAN]): INTEGER_32 -- Number of interval's values that -- satisfy condition require finite: Upper_defined and Lower_defined condition_not_void: condition /= Void ensure non_negative: Result >= 0 feature -- Inapplicable prune (v: INTEGER_32) -- Remove one occurrence of v if any. -- Not applicable here. indexable_put (v: INTEGER_32; k: INTEGER_32) -- Associate value v with key k. -- Not applicable here. invariant count_definition: Upper_defined and Lower_defined implies count = upper - lower + 1 not_infinite: Upper_defined and Lower_defined note copyright: "Copyright (c) 1984-2019, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class INTEGER_INTERVAL
Generated by ISE EiffelStudio