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: Fri, 8 Dec 1995 16:52:42 -0500 From: jcm@mstr.hgc.edu Subject: ARRAY proposal To: NICE-ESG-Libs@atlanta.twr.com ---------- X-Sun-Data-Type: text X-Sun-Data-Description: text X-Sun-Data-Name: text X-Sun-Charset: us-ascii X-Sun-Content-Lines: 67 Please find two files attached: array.library.diffs and array.library The second, array.library, is my proposal for the vintage 96 ARRAY class. Or at least a starting point for such a class. As described in notes in the file itself, I propose almost no new or different functionality. Rather I have just tried to rigorously specify the intent of the vintage 95 ARRAY class. The first file. array.library.diffs (which perhaps should be read first) shows each feature of the vintage 95 ARRAY class followed by the proposed new version, along with occasional notes explaining the changes. These notes are infrequent as I think, based on earlier discussions, that most of the changes are now self explanatory. This proposal has benefited from numerous discussions with folks both inside and outside this forum. I am particularly grateful to Eric Bezault, Roger Browne, Bertrand Meyer, Richard Mitchell, Michael Schweitzer, Steve Tynor, and others whom my addled brain forgets. Thanks also to Christine Mingins for allowing me to post here directly to facilitate discussion. While I would not claim that all the above are in agreement with every comment and assertion in the proposal I think there is very strong consensus with the exception of the feature 'to_c'. In particular there is severe disagreement among the implementers as to the return type of this query. Hence this proposal takes no stand on that issue. The feature 'to_c' is included in the attached files as it appears in vintage 95, but the only inference you should draw from this is that I do not believe the feature should be removed. I'd like the implementers to thrash this problem out and make their own separate motion regarding this issue when they're ready. I have no formal standing on the library committee, but of course that doesn't stop me from having an opinion on how things should proceed :-). 1. First I need someone to move that the proposal be accepted. If no one steps forward soon to do this, I will ask Christine to do so ex officio. 2. I would like to see a deadline set for a vote, say four to six weeks after the proposal has been moved. This deadline can always be extended if discussion warrants. 3. I would like to see proposed changes made in the form of formal amendments each of which can be discussed and voted on. This approach, I hope, satisies both the people who feel we need to look at the big picture (in this case, the whole ARRAY), and those who feel we need to work in small increments. Obviously, the more amendments, the more likely the final vote on the proposal will need to be postponed (which is fine with me as long as people are actively discussing and voting). 4. I would like to see amendments limited to changes to _this_ proposal. In particular, I would prefer not to see suggestions for additional features (unless they can be shown to be tightly coupled to existing ones). The reason for this is that opening discussion on such amendments could easily lead to protracted discussions that would effectively kill the proposal. I think it is important to get a well specified baseline established, after which we can add features that build upon this base. There have been a few comments on this forum recently about the lack of progress and expressing concern as to how the kernel library is to evolve. This proposal gives you a chance to participate and to have a very direct effect on a most fundamental class. Please take full advantage. Might I suggest you start by making a motion? Respectfully submitted, -- Jim McKim ---------- X-Sun-Data-Type: default X-Sun-Data-Name: array.library.diffs X-Sun-Charset: us-ascii X-Sun-Content-Lines: 428 Recommended version of ARRAY with diffs from ELKS95. 12/8/95 Note: The only major changes between this version and what I believe was generally intended in ELKS vintage95 is a new version of the 'make' routine and the splitting of 'resize' into two features. Otherwise, all I'm proposing here is a rigorous specification of the features in (I hope) a readable and forthright way. Special note: The return type of the query "to_c" is causing some controversy among the implementers that may take some time to thrash out. This proposal takes no stand on what that return type should be. The version listed here is that of ELKS95. In each case I show the original version of the feature in ELKS95 and the proposed version. In most cases the motivation for the change is to provide a rigorous specification for the feature in terms of the queries in the specification set (see below). 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] -- Basic specification set: lower, upper, item -- Auxiliary specification set: is_equal, valid_index creation Original: 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.) ensure no_count: (min_index > max_index) implies (count = 0); count_constraint: (min_index <= max_index) implies (count = max_index - min_index + 1) Preferred: 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 + 1 ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default) Original: 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.) Preferred: make_from_array (a: ARRAY [G]) -- Initialize from the values of 'a'. -- Useful in particular when 'a' is a manifest array. -- Note: representation may be shared; to avoid sharing, -- use as "make_from_array(clone( a ))" 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)) Note: There remains some controversy here as some implementers of this feature share underlying representation with the copied array 'a' and others do not, causing obvious interoperability (and perhaps other) problems. In the absence of unanimity, the above warning seems appropriate. 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 + 1 ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default) make_from_array (a: ARRAY [G]) -- Initialize from the items of `a', possibly sharing their representation. -- (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 Original: entry (i: INTEGER): G -- Entry at index i, if in index interval -- (Redefinable synonym for item and infix "@".) require good_key: valid_index (i) Preferred: entry (i: INTEGER): G -- Entry at index i. -- (Redefinable synonym for item and infix "@".) require valid_index: valid_index( i ) Note: The fact that this feature is intended to be redefinable in unpredictable ways makes any postcondition problematic. Original: frozen item (i: INTEGER): G -- Entry at index i, if in index interval require good_key: valid_index (i) Preferred: frozen item (i: INTEGER): G -- Entry at index i. require valid_index: valid_index( i ) Original: frozen infix "@" (i: INTEGER): G -- Entry at index i, if in index interval require good_key: valid_index (i) Preferred: frozen infix "@" (i: INTEGER): G -- Entry at index i. require valid_index: valid_index( i ) ensure definition: Result = item( i ) feature -- Measurement Original: count: INTEGER -- Number of available indices Preferred: count: INTEGER -- Number of available indices ensure definition: Result = upper - lower + 1 Original: lower: INTEGER -- Minimum index Preferred: No Change Original: upper: INTEGER -- Maximum index Preferred: No Change feature -- Comparison Original: is_equal (other: like Current): BOOLEAN -- Is array made of the same items as other? -- (Redefined from GENERAL.) Preferred: 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 Original: valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the array? Preferred: valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the array? ensure -- Defined here as Result = (lower <= i) and (i <= upper) -- May be redefined in descendants. Note: There was some disagreement among the implementers as to whether this feature should remain very fleibly redefinable or not. The comment above is the compromise that resulted. feature -- Element change Original: enter (v: G; i: INTEGER) -- Replace i-th entry, if in index interval, by v. -- (Redefinable synonym for put.) require good_key: valid_index (i) ensure inserted: item (i) = v Preferred: enter (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. -- (Redefinable synonym for put.) require valid_index: valid_index( i ) 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)) Original: 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 Preferred: 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 or else item(n) = item(n).default) new_high_items: -- for_all n, (old upper+1)..(i-1) (item(n) = Void or else item(n) = item(n).default) in_between: -- for_all n, old lower..old upper (i = n or else item(n) = old item(n)) Original: frozen put (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require good_key: valid_index (i) ensure inserted: item (i) = v Preferred: frozen put (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require valid_index: valid_index( i ) 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 Original: resize (minindex, maxindex: INTEGER) -- Rearrange array so that it can accommodate -- indices down to minindex and up to maxindex. -- Do not lose any previously entered item. require valid_indices: minindex <= maxindex ensure no_low_lost: lower = minindex.min (old lower); no_high_lost: upper = maxindex.max (old upper) Preferred: Two different features. One of these, 'accommodate', never shrinks the array. The array stretches if necessary to accommodate the new bounds, never losing any items. The other, 'size', changes the bounds of the array according to its parameters and some items may be lost. The word 'size' should be treated as a verb here (see below). The motivation for this change is that the implementers had interpreted the above comment on 'resize' in these two different ways. accommodate (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. ensure new_lower: lower = min_index.min(old lower) new_upper: upper = max_index.max(old upper) 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 or else item(i) = item(i).default) new_high_items: -- for_all i, (old upper + 1)..upper (item(i) = Void or else item(i) = item(i).default) size(min_index, max_index: INTEGER) -- Resize the array to the given indices. Do not lose -- any item that is in the intersection of the closed -- intervals [lower, upper] and [min_index, max_index]. require valid_indices: min_index <= max_index + 1 ensure new_lower: lower = min_index new_upper: upper = max_index stable_items: -- for_all i, lower..upper ((old lower <= i and i <= old upper) implies item( i ) = old item( i )) new_items: -- for_all i, lower..upper (i < old lower or i > old_upper) implies (item( i ) = Void or else item( i ) = item(i).default)) Note 1: When 'size' is used as a verb it means "to make a particular size; to bring to a proper or suitable size." Note 2: If we only renamed one of these the other implementers' customers would be driven to distraction. Note 3: Once a rigorous specification for 'resize' became available it was immediately clear that different implementers had been interpreting it differently. In addition, it was easy to accommodate (so to speak) both versions. Similar benefits were obtained in homing in on the definition of 'make' in discussions with Roger Browne. I feel good! feature -- Conversion to_c: POINTER -- Address of actual sequence of values, -- for passing to external (non-Eiffel) routines. CONCERN: ISE would like the type of this feature be ANY. Again, the current proposal takes no stand on this issue. feature -- Duplication Original: copy (other: like Current) -- Reinitialize by copying all the items of other. -- (This is also used by clone.) -- (From GENERAL.) Preferred: 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 then -- from GENERAL is_equal: is_equal (other) invariant Original: consistent_size: count = upper - lower + 1; non_negative_count: count >= 0 Preferred: consistent_size: count = upper - lower + 1; nonnegative_count: count >= 0 valid_bounds: lower <= upper + 1 item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i) end ---------- X-Sun-Data-Type: default X-Sun-Data-Name: array.library X-Sun-Charset: us-ascii X-Sun-Content-Lines: 239 Recommended version of ARRAY. 12/8/95 Note: The only major changes between this version and what I believe was generally intended in ELKS vintage95 is a new version of the 'make' routine and the splitting of 'resize' into two features. Otherwise, all I'm proposing here is a rigorous specification of the features in (I hope) a readable and forthright way. Special note: The return type of the query "to_c" is causing some controversy among the implementers that may take some time to thrash out. This proposal takes no stand on what that return type should be. The version listed here is that of ELKS95. 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] -- Basic specification set: lower, upper, item -- Auxiliary specification set: is_equal, valid_index 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 + 1 ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default) make_from_array (a: ARRAY [G]) -- Initialize from the values of 'a'. -- Useful in particular when 'a' is a manifest array. -- Note: representation may be shared; to avoid sharing, -- use as "make_from_array(clone( a ))" 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 + 1 ensure lower_initialized : lower = min_index upper_initialized: upper = max_index items_initialized: -- for_all i, lower..upper (item(i) = Void or else item(i) = item(i).default) make_from_array (a: ARRAY [G]) -- Initialize from the values of 'a'. -- Useful in particular when 'a' is a manifest array. -- Note: representation may be shared; to avoid sharing, -- use as "make_from_array(clone( a ))" 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. -- (Redefinable synonym for item and infix "@".) require valid_index: valid_index( i ) frozen item (i: INTEGER): G -- Entry at index i. require valid_index: valid_index( i ) frozen infix "@" (i: INTEGER): G -- Entry at index i. require valid_index: valid_index( i ) 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 -- Defined here as Result = (lower <= i) and (i <= upper) -- May be redefined in descendants. feature -- Element change enter (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. -- (Redefinable synonym for put.) require valid_index: valid_index( i ) 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 or else item(n) = item(n).default) new_high_items: -- for_all n, (old upper+1)..(i-1) (item(n) = Void or else item(n) = item(n).default) in_between: -- for_all n, old lower..old upper (i = n or else item(n) = old item(n)) frozen put (v: like item; i: INTEGER) -- Replace i-th entry, if in index interval, by v. require valid_index: valid_index( i ) 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 accommodate (min_index, max_index: INTEGER) -- Resize array so that it can accommodate -- indices down to min_index and up to max_index. -- Do not lose any previously entered item. ensure new_lower: lower = min_index.min(old lower) new_upper: upper = max_index.max(old upper) 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 or else item(i) = item(i).default) new_high_items: -- for_all i, (old upper + 1)..upper (item(i) = Void or else item(i) = item(i).default) size(min_index, max_index: INTEGER) -- Resize the array to the given indices. Do not lose -- any item that is in the intersection of the closed -- intervals [lower, upper] and [min_index, max_index]. require valid_indices: min_index <= max_index ensure new_lower: lower = min_index new_upper: upper = max_index stable_items: -- for_all i, lower..upper ((old lower <= i and i <= old upper) implies item( i ) = old item( i )) new_items: -- for_all i, lower..upper (i < old lower or i > old_upper) implies (item( i ) = Void or else item( i ) = item(i).default)) feature -- Conversion to_c: POINTER -- Address of actual sequence of values, -- for passing to external (non-Eiffel) routines. CONCERN: ISE would like the type of this feature be ANY. Again, the current proposal takes no stand on this issue. 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 then -- from GENERAL is_equal: is_equal (other) invariant consistent_size: count = upper - lower + 1; nonnegative_count: count >= 0 valid_bounds: lower <= upper + 1 item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i) end
