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, 17 Aug 1995 10:31:15 GMT From: Roger Browne <rogerb@eiffel.demon.co.uk> Subject: ARRAY 'make' To: NICE-ESG-Libs@atlanta.twr.com Thanks Jim for your useful comments about ARRAY's 'make'. Jim McKim wrote: > Let me put forth three specific possibilities... > > 1) The current version. > > > make (min_index, max_index: 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) I guess what Jim means by "current version" is the current semantics with the addition of his proposed postconditions. For convenient reference, here is the ELS95 version, together with the class invariant: 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) invariant consistent_size: count = upper - lower + 1; non_negative_count: count >= 0 This raises some points: 1. The first postcondition is not as strong is it should be. The LHS is true if and only if the RHS is true, so we could write: no_count: (minindex > maxindex) = (count = 0); 2. The postcondition does not specify what happens to 'upper' and 'lower' when we create an empty array (i.e. minindex > maxindex). Jim's version deliberately overrides 'minindex' and 'maxindex' and sets 'lower' to 0 and 'upper' to -1. This seems counterintuitive. Consider the code fragment: a: ARRAY[X] ... !!a.make(5, 4) a.force(x, 5) It would be very strange if the array range after execution of this code was 0..5 rather than 5..5 I had assumed that the intention of ELS95 was that 'lower' would always be set to 'minindex' and 'upper' to 'maxindex', even in the case of an empty array. But if we allow (as ELS95 does) arbitrary values of 'minindex' and 'maxindex', then the following ELS95 invariant is in error: consistent_size: count = upper - lower + 1; So, clearly ARRAY's 'make' needs to be fixed. This leads us to consider Jim's third case: > 3. A version that allows empty arrays, but with a bit more control than > (1), inspired by Roger's comments > > 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 implies > item(i) = item(i).default) I favour this suggestion, and would suggest one stylistic change to the final, commented, postcondition. change: item(i) /= Void implies item(i) = item(i).default to: item(i) = Void or else item(i) = item(i).default Because I mentally replace 'A implies B' with 'not A or else B', I find the revised wording clearer because it eliminates a double negative. > My current favorite is (3) as Roger has convinced me, but of course that's > for the committee to decide. If (3) is adopted then two invariant > clauses from my earlier proposal, postive_count and valid_bounds, would > have to change. > > nonnegative_count: count >= 0 > valid_bounds: upper + 1 >= lower We can strengthen this by saying more about 'count'. I favour retaining the existing ELS95 invariant (which would now be correct with the new version of 'make'), as follows: consistent_size: count = upper - lower + 1; non_negative_count: count >= 0 Taken together, these imply Jim's 'valid_bounds' invariant, but they say more about 'count'. Jim's third proposal, plus these minor changes, yields an ARRAY 'make' with the following natural semantics: - 'lower' is always set to 'minindex' - 'upper' is always set to 'maxindex' Furthermore, zero-size arrays are permitted, and (unlike the ELS95 version which requires an 'if-then-else'), they do not impose any special case on the implementation of 'count'. Regards, Roger -- -- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525 -- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
