Automatic generation produced by ISE Eiffel
note description: "[ Special objects: homogeneous sequences of values, used to represent arrays and strings ]" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2023-09-06 00:25:14 -0800 (Wed, 06 Sep 2023) $" revision: "$Revision: 107239 $" frozen class interface SPECIAL [T -> ] create make_empty (n: INTEGER_32) -- Create a special object for n entries. require non_negative_argument: n >= 0 ensure capacity_set: capacity = n count_set: count = 0 make_filled (v: T; n: INTEGER_32) -- Create a special object for n entries initialized with v. require non_negative_argument: n >= 0 ensure capacity_set: capacity = n count_set: count = n filled: filled_with (v, 0, n - 1) make_from_native_array (an_array: like native_array) -- Create a special object from an_array. require is_dotnet: {PLATFORM}.is_dotnet an_array_not_void: an_array /= Void feature -- Access at alias "@" (i: INTEGER_32): T -- Item at i-th position. -- (indices begin at 0) require valid_index: valid_index (i) base_address: POINTER -- Address of element at position 0. -- Use only when interfacing with C externals when Current is guaranteed to not move in memory. require not_dotnet: not {PLATFORM}.is_dotnet ensure base_address_not_null: Result /= default_pointer generating_type: TYPE [detachable SPECIAL [T]] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty index_of (v: T; start_position: INTEGER_32): INTEGER_32 -- Index of first occurrence of item identical to v. -- -1 if none. -- (Use object equality for comparison.) require valid_start_position: start_position >= 0 ensure found_or_not_found: Result = -1 or else (Result >= 0 and then Result < count) item alias "[]" (i: INTEGER_32): T assign put -- Item at i-th position. -- (indices begin at 0) require -- from READABLE_INDEXABLE valid_index: valid_index (i) item_address (i: INTEGER_32): POINTER -- Address of element at position i. -- Use only when interfacing with C externals when Current is guaranteed to not move in memory. require not_dotnet: not {PLATFORM}.is_dotnet index_large_enough: i >= 0 index_small_enough: i < count ensure element_address_not_null: Result /= default_pointer native_array: NATIVE_ARRAY [T] -- Only for compatibility with .NET. require is_dotnet: {PLATFORM}.is_dotnet new_cursor: SPECIAL_ITERATION_CURSOR [T] -- Fresh cursor associated with current structure require -- from ITERABLE True ensure -- from ITERABLE result_attached: Result /= Void to_array: ARRAY [T] -- Build an array representation of Current from 1 to `count`. ensure to_array_attached: Result /= Void to_array_lower_set: Result.lower = 1 to_array_upper_set: Result.upper = count feature -- Measurement capacity: INTEGER_32 -- Capacity of special area. ensure -- from ABSTRACT_SPECIAL count_non_negative: Result >= 0 count: INTEGER_32 -- Count of special area. ensure -- from ABSTRACT_SPECIAL count_non_negative: Result >= 0 Lower: INTEGER_32 = 0 -- Minimum index of Current. upper: INTEGER_32 -- Maximum index of Current. feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal alias "≡≡≡" (other: SPECIAL [T]): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) is_equal (other: SPECIAL [T]): BOOLEAN -- Is other attached to an object considered -- equal to current object? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) frozen standard_is_equal alias "≜" (other: SPECIAL [T]): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void filled_with (v: T; start_index, end_index: INTEGER_32): BOOLEAN -- Are all items between index start_index and end_index -- set to v? -- (Use reference equality for comparison.) require start_index_non_negative: start_index >= 0 start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < count same_items (other: like Current; source_index, destination_index, n: INTEGER_32): BOOLEAN -- Are the n elements of other from source_index position the same as -- the n elements of Current from destination_index? -- (Use reference equality for comparison.) require other_not_void: other /= Void source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 n_non_negative: n >= 0 n_is_small_enough_for_source: source_index + n <= other.count n_is_small_enough_for_destination: destination_index + n <= count ensure valid_on_empty_area: n = 0 implies Result same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) valid_index (i: INTEGER_32): BOOLEAN -- Is i within the bounds of Current? require -- from ABSTRACT_SPECIAL True require -- from READABLE_INDEXABLE True ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= upper) feature -- Element change copy_data (other: SPECIAL [T]; source_index, destination_index, n: INTEGER_32) -- Copy n elements of other from source_index position to Current at -- destination_index. Other elements of Current remain unchanged. require other_not_void: other /= Void source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 destination_index_in_bound: destination_index <= count n_non_negative: n >= 0 n_is_small_enough_for_source: source_index + n <= other.count n_is_small_enough_for_destination: destination_index + n <= capacity same_type: other.conforms_to (Current) ensure copied: other /= Current implies same_items (other, source_index, destination_index, n) count_updated: count = (old count).max (destination_index + n) extend (v: T) -- Add v at index `count`. require count_small_enough: count < capacity ensure count_increased: count = old count + 1 same_capacity: capacity = old capacity inserted: item (count - 1) = v extend_filled (v: T) -- Set items between `count` and capacity - 1 with v. ensure same_capacity: capacity = old capacity count_increased: count = capacity filled: filled_with (v, old count, capacity - 1) fill_with (v: T; start_index, end_index: INTEGER_32) -- Set items between start_index and end_index with v. require start_index_non_negative: start_index >= 0 start_index_in_bound: start_index <= count start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < capacity ensure same_capacity: capacity = old capacity count_definition: count = (old count).max (end_index + 1) filled: filled_with (v, start_index, end_index) fill_with_default (start_index, end_index: INTEGER_32) -- Clear items between start_index and end_index. require is_self_initializing: ({T}).has_default start_index_non_negative: start_index >= 0 start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < count ensure filled: filled_with (({T}).default, start_index, end_index) force (v: T; i: INTEGER_32) -- If i is equal to `count` increase `count` by one and insert v at index `count`, -- otherwise replace i-th item by v. -- (Indices begin at 0.) require index_large_enough: i >= 0 index_small_enough: i <= count not_full: i = count implies count < capacity ensure count_updated: count = (i + 1).max (old count) same_capacity: capacity = old capacity inserted: item (i) = v insert_data (other: SPECIAL [T]; source_index, destination_index, n: INTEGER_32) -- Insert n elements of other from source_index position to Current at -- destination_index and shift elements between destination_index and `count` -- to the right. Other elements of Current remain unchanged. require other_not_void: other /= Void source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 destination_index_in_bound: destination_index <= count n_non_negative: n >= 0 n_is_small_enough_for_source: source_index + n <= other.count n_is_small_enough_for_destination: count + n <= capacity same_type: other.conforms_to (Current) ensure copied: same_items (other, source_index, destination_index, n) count_updated: count = old count + n move_data (source_index, destination_index, n: INTEGER_32) -- Move n elements of Current from source_start position to destination_index. -- Other elements remain unchanged. require source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 destination_index_in_bound: destination_index <= count n_non_negative: n >= 0 n_is_small_enough_for_source: source_index + n <= count n_is_small_enough_for_destination: destination_index + n <= capacity ensure moved: same_items (old twin, source_index, destination_index, n) count_updated: count = (old count).max (destination_index + n) non_overlapping_move (source_index, destination_index, n: INTEGER_32) -- Move n elements of Current from source_start position to destination_index. -- Other elements remain unchanged. require source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 destination_index_in_bound: destination_index <= count n_non_negative: n >= 0 different_source_and_target: source_index /= destination_index non_overlapping: (source_index < destination_index implies source_index + n < destination_index) or (source_index > destination_index implies destination_index + n < source_index) n_is_small_enough_for_source: source_index + n <= count n_is_small_enough_for_destination: destination_index + n <= capacity ensure moved: same_items (Current, source_index, destination_index, n) count_updated: count = (old count).max (destination_index + n) overlapping_move (source_index, destination_index, n: INTEGER_32) -- Move n elements of Current from source_start position to destination_index. -- Other elements remain unchanged. require source_index_non_negative: source_index >= 0 destination_index_non_negative: destination_index >= 0 destination_index_in_bound: destination_index <= count n_non_negative: n >= 0 different_source_and_target: source_index /= destination_index n_is_small_enough_for_source: source_index + n <= count n_is_small_enough_for_destination: destination_index + n <= capacity ensure moved: same_items (old twin, source_index, destination_index, n) count_updated: count = (old count).max (destination_index + n) put (v: T; i: INTEGER_32) -- Replace i-th item by v. -- (Indices begin at 0.) require index_large_enough: i >= 0 index_small_enough: i < count ensure inserted: item (i) = v same_count: count = old count same_capacity: capacity = old capacity feature -- Removal replace_all (v: T) -- Replace all items with v. ensure cleared: filled_with (v, 0, upper) wipe_out -- Reset count to zero. ensure same_capacity: capacity = old capacity count_reset: count = 0 feature -- Resizing aliased_resized_area (n: INTEGER_32): like Current -- Try to resize Current with a count of n, if not -- possible a new copy. require n_non_negative: n >= 0 ensure result_not_void: Result /= Void new_count: Result.count = n.min (old count) new_capacity: Result.capacity = n preserved: Result.same_items (old twin, 0, 0, n.min (old count)) aliased_resized_area_with_default (a_default_value: T; n: INTEGER_32): like Current -- Try to resize Current with a count of n, if not -- possible a new copy. Non yet initialized entries are set to a_default_value. require n_non_negative: n >= 0 ensure result_not_void: Result /= Void new_count: Result.count = n new_capacity: Result.capacity = n preserved: Result.same_items (old twin, 0, 0, n.min (old count)) keep_head (n: INTEGER_32) -- Keep the first n entries. require non_negative_argument: n >= 0 less_than_count: n <= count ensure count_updated: count = n kept: same_items (old twin, 0, 0, n) keep_tail (n: INTEGER_32) -- Keep the last n entries. require non_negative_argument: n >= 0 less_than_count: n <= count ensure count_updated: count = n kept: same_items (old twin, n, 0, n) remove_head (n: INTEGER_32) -- Remove the first n entries. require non_negative_argument: n >= 0 less_than_count: n <= count ensure count_updated: count = old count - n kept: same_items (old twin, n, 0, count) remove_tail (n: INTEGER_32) -- Keep the first count - n entries. require non_negative_argument: n >= 0 less_than_count: n <= count ensure count_updated: count = old count - n kept: same_items (old twin, 0, 0, count) resized_area (n: INTEGER_32): like Current -- A copy of Current with a count of n. require n_non_negative: n >= 0 ensure result_not_void: Result /= Void result_different_from_current: Result /= Current new_count: Result.count = n.min (old count) new_capacity: Result.capacity = n preserved: Result.same_items (Current, 0, 0, n.min (old count)) resized_area_with_default (a_default_value: T; n: INTEGER_32): like Current -- Create a copy of Current with a count of n where not yet initialized -- entries are set to a_default_value. require n_non_negative: n >= 0 ensure result_not_void: Result /= Void result_different_from_current: Result /= Current new_count: Result.count = n new_capacity: Result.capacity = n preserved: Result.same_items (Current, 0, 0, n.min (old count)) feature -- Duplication copy (other: SPECIAL [T]) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other frozen deep_copy (other: SPECIAL [T]) -- Effect equivalent to that of: -- `copy` (other . `deep_twin`) -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY deep_equal: deep_equal (Current, other) frozen deep_twin: SPECIAL [T] -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) frozen standard_copy (other: SPECIAL [T]) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_standard_equal: standard_is_equal (other) frozen standard_twin: SPECIAL [T] -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) frozen twin: SPECIAL [T] -- New object equal to Current -- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations frozen default: detachable SPECIAL [T] -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.`default` for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class feature -- Iteration do_all_in_bounds (action: PROCEDURE [T]; start_index, end_index: INTEGER_32) -- Apply action to every item, from first to last. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. require action_not_void: action /= Void do_all_with_index_in_bounds (action: PROCEDURE [T, INTEGER_32]; start_index, end_index: INTEGER_32) -- Apply action to every item, from first to last. -- action receives item and its index. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. require action_not_void: action /= Void do_if_in_bounds (action: PROCEDURE [T]; test: FUNCTION [T, BOOLEAN]; start_index, end_index: INTEGER_32) -- Apply action to every item that satisfies test, from first to last. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. require action_not_void: action /= Void test_not_void: test /= Void do_if_with_index_in_bounds (action: PROCEDURE [T, INTEGER_32]; test: FUNCTION [T, INTEGER_32, BOOLEAN]; start_index, end_index: INTEGER_32) -- Apply action to every item that satisfies test, from first to last. -- action and test receive the item and its index. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. require action_not_void: action /= Void test_not_void: test /= Void for_all_in_bounds (test: FUNCTION [T, BOOLEAN]; start_index, end_index: INTEGER_32): BOOLEAN -- Is test true for all items? require test_not_void: test /= Void there_exists_in_bounds (test: FUNCTION [T, BOOLEAN]; start_index, end_index: INTEGER_32): BOOLEAN -- Is test true for at least one item? require test_not_void: test /= Void feature -- Output debug_output: STRING_8 -- String that should be displayed in debugger to represent Current. require -- from DEBUG_OUTPUT True ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void invariant consistent_count: count = upper - Lower + 1 -- from ABSTRACT_SPECIAL count_less_than_capacity: count <= capacity -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= upper or else Lower = upper + 1 note copyright: "Copyright (c) 1984-2023, 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 SPECIAL -- Generated by Eiffel Studio --
For more details: eiffel.org