NICE-ESG-Libs Digest Wed, 13 Dec 95 Volume 1 : Issue 320
Today's Topics:
Meaning of 'meaningful'
NICE-ESG-Libs Digest V1 #319
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 01:11:40 +0000
From: Roger Browne
Subject: Meaning of 'meaningful'
To: NICE-ESG-Libs@atlanta.twr.com
> In NICE-ESG-Libs Digest Issue 318 Steve Tynor wrote:
> Also, I may be being dense, but what does Roger mean by:
>
> | entirety. However, when the non-executable part is commented out,
> | the remaining subexpression does not yield a meaningful result when
> | evaluated.
>
> When the non-executable part is commented out, the remaining result is a
> subset of the postcondition's promise. It's meaningful, just not the
> whole story.
Sorry for any confusion, maybe 'meaningful' is not the correct word.
The execution of the remaining subexpression certainly has 'meaning',
but that meaning is not correct or useful from the point of view of
an executable postcondition.
If we consider the executable part...
ensure
definition: Result = (lower = other.lower) and (upper = other.upper)
...then when we are comparing two arrays that have identical upper
and lower bounds but different contents, the subexpression implies
that 'Result' should be true whereas the semantics of 'is_equal'
requires that 'Result' must be false.
Regards,
Roger
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
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.
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.
Regards,
Roger
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: compilers/libraries/publications | +44-1772-687525
|
|
