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: Thu, 25 May 95 23:32:20 BST From: Simon Parker <sparker@eiffel.ie> Subject: Array recommendations, from Jim McKim To: NICE Libraries Committee <NICE-ESG-Libs@atlanta.twr.com> --VERSION:801442377:455017068:445055017:-1375681016 Content-Type: TEXT/PLAIN; charset=US-ASCII Delegates, Jim McKim sent this thoughtful piece of work to me, with a request that I pass it on to the Library committee. Although Christine is paying close attention to Library committee matters, her temporary electronic mail facilities in Europe would make the task of relaying messages arduous. I have posted this message on her behalf, boldly assuming her approval and yours. If this breach of rules and etiquette is unjustified, please forgive me. In any case, it will not become a habit. Regards, Simon - - - - - - - - - - Simon Parker Eiffel Ireland (Consultancy, training, compilers, books) 45 Hazelwood, Shankill, Co Dublin, Ireland (+353 1) 282 3487 sparker@eiffel.ie http://www.eiffel.ie/Eiffel/ ------------------------------ Begin quote ------------------------------------------ To the Library Committee. Accompanying this document please find proposed changes to the flat-short form of the ARRAY class. As I am not a member of the Committee, this is not a formal proposal. I hope that one or more of you will see sufficient merit in this work that you will sponsor the proposal yourselves. Motivation: ARRAY and STRING are among the first classes that people learning Eiffel will see. As such it is especially important that these classes are well documented and well specified via preconditions, postconditions, and assertions. Right now the following scenario is all too typical: 1) I espouse the marvelous benefits of programming by contract as a tool for documenting class libraries so that readers can understand classes _without_ reading the code. 2) Students look at the short form of ARRAY, specifically at "make" and ask, "Where are my min_index and max_index parameters saved?" 3) I answer, "In lower and upper." 4) They retort, "How do you know?" 5) I reply sheepishly, "I looked at the code." As many of you know I've been interested in and writing about Programming by Contract for some time and have developed some criteria for applying it well. The result of applying these criteria to the ARRAY class is what you have before you. In all but one or two cases I have not recommended any changes that would affect the implementation of a feature. I've just tried to give clear and complete pre and postconditions that specify the _current_ behavior. There are actually three files that accompany this document. These are 1) The original version, array.original, taken from the ASCII directory at ISE's ftp site on May 24. The ONLY difference between what you have here and what was at ISE on that date is that I've reformatted the former for easier reading. 2) The recommended diff's version, array.recs. This version shows the original short form for each feature, then my preferred form and then some justifications for the recommended changes. 3) The "final" version, array.done. This version just includes my preferred spec's for each feature i.e no original versions, no justifications. Assumption: I have assumed that comments within assertion clauses show up in the short form. Not all vendors support this at the moment, although I don't believe any are averse to providing such support in the future. A little bit on the criteria I used: 1) Pick a small set of queries to use as a "specification set". For ARRAY, the specification set consists of lower, upper, and item. Each command specifies precisely how it affects the value of each of these queries, whether it changes those values or not. 2) Each query not in the specification set is specified in terms of values in that set. 3) You will see comments of the form for_all i, min..max (some_assertion). This structure asserts that "some_assertion" is true for each integer i from min up to max. If min > max then the overall assertion is true. 4) Blatant Plug: To find out more about these criteria, come to my Tutorial at either TOOLS USA or OOPSLA :-). I hope you will take some time to look these suggested changes over and that you will accept them by acclamation :-). Please contact me with any questions or concerns. Best regards, -- Jim McKim -----------------------------------End quote ------------------------------------- (Attachments in another message, or below) --VERSION:801442377:455017068:445055017:-1375681016 Content-Type: TEXT/PLAIN; SizeOnDisk=27723; name="JCMARRAY.TXT"; CHARSET=US-ASCII Content-Description: Three files from Jim McKim ---------- X-Sun-Data-Type: default X-Sun-Data-Name: array.original X-Sun-Content-Lines: 146 Original version -- array.original 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] creation make (minindex, maxindex: INTEGER) -- Allocate array; set index interval to -- minindex .. maxindex; set all values to default. -- (Make array empty if minindex > maxindex.) ensure no_count: (minindex > maxindex) implies (count = 0); count_constraint: (minindex <= maxindex) implies (count = maxindex - minindex + 1) 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.) feature -- Initialization make (minindex, maxindex: INTEGER) -- Set index interval to minindex .. maxindex; -- reallocate if necessary; set all values to default. -- (Make array empty if minindex > maxindex.) ensure no_count: (minindex > maxindex) implies (count = 0); count_constraint: (minindex <= maxindex) implies (count = maxindex - minindex + 1) make_from_array (a: ARRAY [G]) -- Initialize from the items of a; reallocate if -- necessary. (Useful in proper descendants of -- class ARRAY, to initialize an array-like object -- from a manifest array.) feature -- Access entry (i: INTEGER): G -- Entry at index i, if in index interval -- (Redefinable synonym for item and infix "@".) require good_key: valid_index (i) frozen item (i: INTEGER): G -- Entry at index i, if in index interval require good_key: valid_index (i) frozen infix "@" (i: INTEGER): G -- Entry at index i, if in index interval require good_key: valid_index (i) feature -- Measurement count: INTEGER -- Number of available indices 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.) feature -- Status report valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the array? feature -- Element change 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 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 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 feature -- Resizing 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 good_indices: minindex <= maxindex ensure no_low_lost: lower = minindexlmin (old lower); no_high_lost: upper = maxindexlmax (old upper) 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.) invariant consistent_size: count = upper - lower + 1; non_negative_count: count >= 0 end ---------- X-Sun-Data-Type: default X-Sun-Data-Name: array.recs X-Sun-Content-Lines: 521 Recommended changes with justifications. -- array.recs 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] Preferred: Add comment that gives the set of features used for specifying the class. -- Specification set: lower, upper, item creation Original: make (minindex, maxindex: INTEGER) -- Allocate array; set index interval to -- minindex .. maxindex; set all values to default. -- (Make array empty if minindex > maxindex.) ensure no_count: (minindex > maxindex) implies (count = 0); count_constraint: (minindex <= maxindex) implies (count = maxindex - minindex + 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 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) Justification and Notes: 1) Enforce usual notation conventions i.e. min_index instead of minindex. 2) Why no precondition in the original version? Are we really doing users a favor by letting them call make( 7, -10 ) and giving them an array with lower = 0 and upper = -1? This change could break some code, but it's almost certainly code that shouldn't exist anyway. (He said arrogantly :-)). 3) The old postcondition tells us about count. IMHO, lower, upper, and item are more important. count can be handled in terms of these. Special Note: Hers's a compromise version if we can't change the precondition. make (minindex, maxindex: INTEGER) -- Allocate array; set index interval to -- minindex .. maxindex; set all values to default. -- (Make array empty if minindex > maxindex.) ensure no_items: min_index > max_index implies (lower = 0 and upper = -1) lower_initialized : min_index <= max_index implies lower = min_index upper_initialized: min_index <= max_index implies upper = max_index items_initialized: -- for_all i, lower..upper (item(i) /= Void implies item(i) = item(i).default) Justification and Notes: 1) If we're gonna let 'em send a bad min_index, max_index combination, let's at least tell 'em what really happens. 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 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)) Justification and Notes: 1) Include precondition for safety, clarity, simplicity. 2) Have the postconditions say what happens. feature -- Initialization Special Note: I assume these two features are repeated here as they are both public and creation features. Naturally my recommendations and reasoning are the same as above. I haven't repeated the Justifications. Original: make (minindex, maxindex: INTEGER) -- Set index interval to minindex .. maxindex; -- reallocate if necessary; set all values to default. -- (Make array empty if minindex > maxindex.) ensure no_count: (minindex > maxindex) implies (count = 0); count_constraint: (minindex <= maxindex) implies (count = maxindex - minindex + 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 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) 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 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 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, if in index interval -- (Redefinable synonym for item and infix "@".) require large_enough: i >= lower small_enough: i <= upper ensure Result = item( i ) Justification and Notes: 1) By using upper and lower here we can keep the specification set small. 2) Also valid_index is not well specified so is not a sufficient precondition 3) Will descendants want a different postcondition? (!) If we want to allow that possibility then we should omit this one or make it a comment. 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, if in index interval require large_enough: i >= lower small_enough: i <= upper Justification and Notes: 1) By using upper and lower here we can keep the specification set small. 2) Also valid_index is not well specified so is not a sufficient precondition 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, if in index interval require large_enough: i >= lower small_enough: i <= upper ensure Result = item( i ) Justification and Notes: 1) By using upper and lower here we can keep the specification set small. 2) Also valid_index is not well specified so is not a sufficient precondition. 3) Need postcondition to map this feature to specification set. feature -- Measurement Original: count: INTEGER -- Number of available indices Preferred: count: INTEGER -- Number of available indices ensure Result = upper - lower + 1 Justification and Notes: 1) Need to say what the Result is. 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 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) Justification and Notes: 1) I think the missing precondition in the original is an error as it's in GENERAL. 2) The postcondition just tells it like it is - I hope. 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 Result = (lower <= i) and (i <= upper) Justification and Notes: 1) Just tell 'em the precise truth. 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: 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)) Justification and Notes: 1) Same notes on replacing valid_index as before. 2) If you haven't seen this flavor of postcondition before, it looks a lot heavier than it is. While this is clearly correct for put, I suppose it may be too much here, depending on how much leeway we're willing to allow descendants. 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; stable_before_i: i <= old upper implies for_all n, (old lower)..(i-1) (item(n) = old item(n)) stable_after_i: i >= old lower implies for_all n, (i+1)..(old upper) (item(n) = old item(n)) new_lower: i < old lower implies lower = i new_low_items -- i < old lower implies for_all n, (lower+1)..(old lower-1) (item(n) /= Void implies item(n) = item(n).default) new_upper: i > old upper implies upper = i new_high_items -- i > old upper implies for_all n, (old upper)..(upper-1) (item(n) /= Void implies item(n) = item(n).default) Justification and Notes: 1) This looks complex 'cause it is :-) It's basically what happens when the supplier takes on the entire contract. Special Note: If I had my druthers I'd lose this feature. If clients want to expand the ARRAY, let 'em call resize first. But maybe that's just the control freak in me coming out.... I've kept this feature in the "finished" version. 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 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)) Justification and Notes: 1) Usual comments on replacing valid_index in the precondition. 2) The postcondition just speaks the truth. 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: 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) Justification and Notes: 1) While it's not entirely clear from the original short, it's clear from both Tower's and ISE's code that the array is not allowed to shrink from either end. The new precondition just makes that explicit. 2) And the new postcondition just makes it real clear what happens. feature -- Conversion Original: to_c: POINTER -- Address of actual sequence of values, -- for passing to external (non-Eiffel) routines. Preferred: No Change. Anyone who wants to mess around with C pretty much has to expect to look at the code. 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 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) Justification and Notes: 1) Again I believe the absence of the precondition in the original is an error. 2) Again the postcondition just says what really happens. The old postcondition from GENERAL really does the job, but I do like specifying directly in terms of the specification set. Original: invariant consistent_size: count = upper - lower + 1; non_negative_count: count >= 0 Preferred: 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)) Justification and Notes: 1) Stronger assertions assume the preferred versions of make and make_from_array are adopted. 2) Also have assumed entry's we do not want descendants to change the Result of the call. end ---------- X-Sun-Data-Type: default X-Sun-Data-Name: array.done X-Sun-Content-Lines: 219 Preferred version of ARRAY. -- array.done 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 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 Result = item( i ) feature -- Measurement count: INTEGER -- Number of available indices ensure 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 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 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; stable_before_i: i <= old upper implies for_all n, (old lower)..(i-1) (item(n) = old item(n)) stable_after_i: i >= old lower implies for_all n, (i+1)..(old upper) (item(n) = old item(n)) new_lower: i < old lower implies lower = i new_low_items -- i < old lower implies for_all n, (lower+1)..(old lower-1) (item(n) /= Void implies item(n) = item(n).default) new_upper: i > old upper implies upper = i new_high_items -- i > old upper implies for_all n, (old upper)..(upper-1) (item(n) /= Void implies item(n) = item(n).default) 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 --VERSION:801442377:455017068:445055017:-1375681016--
Date: Thu, 25 May 95 15:15:25 -0400 From: Jason Schroeder <shrode@wsc.com> Subject: Jason explains yesterday's odd message To: NICE-ESG-Libs@atlanta.twr.com Dear Library Committee, A letter of mine accidentally went to the committee mailing list instead of its intended recipient. I was responding to a lobbyist for Mr. Johnson as chair. I did not intend to share my abruptness with the committee. I carry no disrespect for the committee or the chair and apologise for any distress I might have caused my fellow members and the Eiffel community at large. I intend to be an active and trustworthy member - I like Eiffel, otherwise I would not be here. I wish my initial act with the committee would have been a formal introduction of myself and my views rather than writing this letter. That will be coming soon. As usual, there are reasons to vote and not vote for both candidates. If somebody wishes to discuss these options with me, I will reply - and I will not use the wrong keystrokes in Emacs to reply ;-) Jason Schroeder
