NICE-ESG-Libs Digest Thu, 17 Aug 95 Volume 1 : Issue 285
Today's Topics:
NICE-ESG-Libs Digest V1 #284
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:02:16 -0400
From: jcm@mstr.hgc.edu
Subject: NICE-ESG-Libs Digest V1 #284
To: NICE-ESG-Libs@atlanta.twr.com
> From root@atlanta.twr.com Thu Aug 17 08:47:51 1995
> Reply-To: NICE-ESG-Libs@atlanta.twr.com
> Subject: NICE-ESG-Libs Digest V1 #284
> To: NICE-ESG-Libs---DO-REPLY-TO-THIS-ADDRESS@atlanta.twr.com
> Content-Length: 5542
> X-Lines: 154
>
>
> NICE-ESG-Libs Digest Thu, 17 Aug 95 Volume 1 : Issue 284
>
> Today's Topics:
> ARRAY 'make'
>
> ----------------------------------------------------------------------
> 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
> Subject: ARRAY 'make'
> To: NICE-ESG-Libs@atlanta.twr.com
>
> Thanks Jim for your useful comments about ARRAY's 'make'.
And the same to you :-).
>
> 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.
I should have made this clearer. By "current version" I meant what Tower and
ISE's implementations currently do. That is, I was simply trying to codify
existing practice.
[.. Roger notes some problems with the "current version" ..]
>
> 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.
I have no problem with this. In fact I agree that it is clearer in this
particular case.
If we can get a bit more discussion from folks, I'll incorporate what I take
to be consensus changes and then try to convince _somebody_ (hint, hint) on
the Committee to officially propose the full specification.
>
> > 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'.
Yup. I only showed the clauses that needed to _change_ as a result of this
change to "make". For the remainder of the invariant, including consistent_size,
see the full proposal most recently posted to this group on 3 July.
[.. Roger says nice things about the third version of "make" ..]
>
> Regards,
> Roger
> --
> -- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
> -- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
>
> ==================================================
>
> End of NICE-ESG-Libs Digest
> ******************************
>
Best,
-- Jim
 |
