NICE-ESG-Libs Digest Wed, 13 Dec 95 Volume 1 : Issue 321
Today's Topics:
NICE-ESG-Libs Digest V1 #320
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: Wed, 13 Dec 1995 10:18:15 -0500
From: jcm@mstr.hgc.edu
Subject: NICE-ESG-Libs Digest V1 #320
To: NICE-ESG-Libs@atlanta.twr.com
> From root@atlanta.twr.com Wed Dec 13 06:48:45 1995
> Reply-To: NICE-ESG-Libs@atlanta.twr.com
> Subject: NICE-ESG-Libs Digest V1 #320
> To: NICE-ESG-Libs---DO-NOT-REPLY-TO-THIS-ADDRESS@atlanta.twr.com
> Content-Length: 4180
> X-Lines: 113
>
>
> NICE-ESG-Libs Digest Wed, 13 Dec 95 Volume 1 : Issue 320
>
> Today's Topics:
> Meaning of 'meaningful'
> NICE-ESG-Libs Digest V1 #319
>
[...]
>
> Date: Wed, 13 Dec 1995 00:15:16 +0000
> >From: Roger Browne
> Subject: NICE-ESG-Libs Digest V1 #319
> To: NICE-ESG-Libs@atlanta.twr.com
>
> In NICE-ESG-Libs Digest V1 #317 Bertrand Meyer wrote:
>
> > Postcondition of is_equal:
> >
> > The diagnostic is right but the cure is worth than the disease.
> > Making the whole assertion into the postcondition is overkill.
> >
> > I suggest:
> >
> > ensure
> > same_bounds: Result implies (lower = other.lower) and (upper = other.upper)
> > same_elements: -- Result = (lower = other.lower) and (upper = other.upper) and for_all i, lower..upper (item(i) = other.item(i))
>
> When I first emailed Jim about this, I suggested the same as you have
> here (with different tag names). However, Jim has convinced me that:
>
> - The purpose of the Eiffel Library Standard is to _specify_,
> and that purpose is served perfectly by the commented postcondition.
>
> - It's up to the implementors what kind of runtime checking they
> provide to help ensure compliance with the specification.
> (Some might provide none, on the assumption that the kernel
> classes are well tested. Others might find a way to check at
> runtime the full postcondition including the 'for all' part.)
> This is a quality issue, not a standards issue: an implementation
> might execute the postconditions without failure yet still be
> incorrect because the postconditions are not exhaustive, whilst
> another implementation might execute no postconditions at all
> yet be correct.
>
> This principle might be called "separate the specification from the
> runtime testing", and I feel it will lead to tighter, more readable
> specifications.
Very well said.
>
> Procedurally, if amendment RB-3 fails, someone can move a further
> amendment to RB-2 (Jim's ARRAY proposal) along the lines of Bertrand's
> suggestion.
Just a clarification. I hope everyone will vote for RB-3 as it clearly
corrects an error in the original. If you are not dazzled by my poor
argument combined with Roger's eloquent one, then you are free to offer
an amendment that would add the runtime check regardless of whether RB-3
passes or fails. However, I do think that, procedurally, we should dispose
of RB-3 before taking up any conflicting motions.
In case someone does plan to offer an amendment adding the runtime check
(again I do not favor this, but just in case)
I would prefer something like the following. This is called "hedging one's
bet" in America :-):
ensure
definition: -- Result = (lower = other.lower) and (upper = other.upper) and for_all i, lower..upper (item(i) = other.item(i))
same_bounds: Result implies (lower = other.lower) and (upper = other.upper)
-- Partial runtime check added as the full specification is not automatically checkable.
> Regards,
> Roger
> --
> -- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
> -- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
>
> ==================================================
Best,
-- Jim
>
> End of NICE-ESG-Libs Digest
> ******************************
>
 |
