NICE Eiffel Standards Group -- Library Committee Mailing List To post to list: NICE-ESG-Libs@atlanta.twr.com To send mail to the Chairman of the committee: NICE-ESG-Libs-chair@atlanta.twr.com Administrative matters (sign up, unsubscribe, mail problems, etc): NICE-ESG-Libs-request@atlanta.twr.com
Date: Mon, 03 Jul 1995 22:38:51 +1000 (EST) From: cmingins@insect.sd.monash.edu.au (Christine Mingins) Subject: Array Redux Redux To: NICE-ESG-Libs@atlanta.twr.com Jim McKim has posted an amended specification of ARRAY for your consideration. He is also inviting comments on this approach. His posting is attached below. -- Christine ---------------------------------------------------------------------- To the Library Committee: The attached version of the ARRAY specification includes a cosmetic change and a correction to the postcondition on 'force'. These changes are detailed out in the text. Please use this version in place of the one titled array.done that I sent you earlier. I'm working on a similar specification of STRING, but will not bother the Committee with it until I can gauge your interest in this approach. I'm looking forward to discussing these specifications with you and, of course, hope that one or more of you will champion this work to be part of Vintage '96. Best, -- Jim Preferred version of ARRAY. -- array.fixed Changes since previous version (array.done). 1. There is a new postcondition on 'force' which has two advantages over the previous version. a) It is correct :-). b) It is simpler. 2. Previously there were no labels on postconditions of queries that were in the form Result = .... I've now adopted the convention that such assertions are labeled 'definition:' and have changed the below accordingly. Class ARRAY indexing description: "Sequences of values, all of the same type or of a conforming one, accessible through integer indices in a contiguous interval" class interface ARRAY [G] -- Specification set: lower, upper, item creation make (min_index, max_index: INTEGER) -- Allocate array; set index interval to -- min_index .. max_index; set all values to default. require valid_indices: min_index <= max_index ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) /= Void implies item(i) = item(i).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 a_not_void: a /= Void ensure lower_initialized : lower = a.lower upper_initialized: upper = a.upper items_initialized: -- for_all i, lower..upper (item(i) = a.item(i)) feature -- Initialization make (min_index, max_index: INTEGER) -- Allocate array; set index interval to -- min_index .. max_index; set all values to default. require valid_indices: min_index <= max_index ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) /= Void implies item(i) = item(i).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 a_not_void: a /= Void ensure lower_initialized : lower = a.lower upper_initialized: upper = a.upper items_initialized: -- for_all i, lower..upper (item(i) = a.item(i)) feature -- Access entry (i: INTEGER): G -- Entry at index i, if in index interval -- (Redefinable synonym for item and infix "@".) require large_enough: i >= lower small_enough: i <= upper ensure definition: Result = item( i ) frozen item (i: INTEGER): G -- Entry at index i, if in index interval require large_enough: i >= lower small_enough: i <= upper frozen infix "@" (i: INTEGER): G -- Entry at index i, if in index interval require large_enough: i >= lower small_enough: i <= upper ensure definition: Result = item( i ) feature -- Measurement count: INTEGER -- Number of available indices ensure definition: Result = upper - lower + 1 lower: INTEGER -- Minimum index upper: INTEGER -- Maximum index feature -- Comparison is_equal (other: like Current): BOOLEAN -- Is array made of the same items as other? -- (Redefined from GENERAL.) require else -- from GENERAL other_not_void: other /= Void ensure definition: Result = (lower = other.lower) and (upper = other.upper) --and for_all i, lower..upper (item( i ) = other.item( i )) ensure then -- from GENERAL consistent: standard_is_equal (other) implies Result; same_type: Result implies same_type (other); symmetric: Result implies other.is_equal (Current) feature -- Status report valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the array? ensure definition: Result = (lower <= i) and (i <= upper) feature -- Element change enter (v: G; i: INTEGER) -- Replace i-th entry, if in index interval, by v. -- (Redefinable synonym for put.) require index_large_enough: i >= lower index_small_enough: i <= upper ensure stable_lower: lower = old lower stable_upper: upper = old upper new_item: item(i) = v stable_before_i: -- for_all n, lower..(i-1) (item(n) = old item(n)) stable_after_i: -- for_all n, (i+1)..upper (item(n) = old item(n)) 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 new_item: item (i) = v; new_lower: lower = i.min( old lower ) new_upper: upper = i.max( old upper ) new_low_items: -- for_all n, (i+1)..(old lower-1) (item(n) /= Void implies item(n) = item(n).default) new_high_items: -- for_all n, (old upper+1)..(i-1) (item(n) /= Void implies item(n) = item(n).default) in_between: -- for_all n, old lower..old upper (i /= n implies item(n) = old item(n)) frozen put (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require index_large_enough: i >= lower index_small_enough: i <= upper ensure stable_lower: lower = old lower stable_upper: upper = old upper new_item: item(i) = v stable_before_i: -- for_all n, lower..(i-1) (item(n) = old item(n)) stable_after_i: -- for_all n, (i+1)..upper (item(n) = old item(n)) feature -- Resizing 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 valid_min_index: min_index <= lower valid_max_index: max_index >= upper ensure new_lower: lower = min_index new_upper: upper = max_index stable_items: -- for_all i, (old lower)..(old upper) (item(i) = old item(i)) new_low_items: -- for_all i, lower..(old lower - 1) (item(i) /= Void implies item(i) = item(i).default) new_high_items: -- for_all i, (old upper + 1)..upper) (item(i) /= Void implies item(i) = item(i).default) feature -- Conversion to_c: POINTER -- 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.) -- (From GENERAL.) require else --from GENERAL other_not_void: other /= Void ensure new_lower: lower = other.lower new_upper: upper = other.upper new_items: -- for_all i, lower..upper (item(i) = other.item(i) ensure then -- from GENERAL is_equal: is_equal (other) invariant consistent_size: count = upper - lower + 1; positive_count: count >= 1 valid_bounds: upper >= lower valid_indices: -- for_all i:INTEGER (valid_index(i) = (lower <= i and i <= upper) item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i) item_equals_entry: -- for_all i, lower..upper (item( i ) = entry(i)) end
