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: Tue, 12 Dec 1995 16:37:48 -0500 From: jcm@mstr.hgc.edu Subject: NICE-ESG-Libs Digest V1 #317 To: NICE-ESG-Libs@atlanta.twr.com > From root@atlanta.twr.com Tue Dec 12 15:24:41 1995 > Reply-To: NICE-ESG-Libs@atlanta.twr.com > Subject: NICE-ESG-Libs Digest V1 #317 > To: NICE-ESG-Libs---DO-NOT-REPLY-TO-THIS-ADDRESS@atlanta.twr.com > Content-Length: 1407 > X-Lines: 46 > > > NICE-ESG-Libs Digest Tue, 12 Dec 95 Volume 1 : Issue 317 > > Today's Topics: > NICE-ESG-Libs Digest V1 #316 > > ---------------------------------------------------------------------- > 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: Tue, 12 Dec 95 19:23:51 GMT > >From: bertrand@eiffel.fr (Bertrand Meyer @ SOL) > Subject: NICE-ESG-Libs Digest V1 #316 > To: NICE-ESG-Libs@atlanta.twr.com > > 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)) > > > The second clause is the one suggested in RB-3, with a different label. > (I don't really care about the label, however.) Both Roger himself and Michael Schweitzer have made the same suggestion to me. I would prefer the specification remain as in Roger's original amendment, but can certainly live with the change (without a vote I have little choice :-)). (Side note: just as I was about to send this, Steve weighed in, agreeing with Bertrand.) I prefer the original version to the one above as the latter is clearly redundant. The assertion, "same_elements" gives the full specification. The assertion, "same_bounds" has been added to provide a partial runtime check. Now I have no objection to adding such runtime checks when one is verifying the correctness of software, but my goal with ARRAY was, and remains, first and foremost, to provide assertions necessary to _specify_ the features. If such assertions can be compiled into runtime checks then so much the better, but I have tried not to include runtime checks that are redundant with rigorous comments, as Bertrand is suggesting here. As I see it, such redundant checks are useful for developers looking for bugs in the code, but in fact are useless to clients for whom the rigorous comment says it all. Actually it can be even worse than useless. Sometimes the client will be confused by the redundant assertion, assuming she's missing something because she can't see what it contributes. This could be ameliorated, I suppose, by using a label or adding a comment that documents the check as redundant. Another reason for excluding such checks is that once you start to do so it is difficult to know when to stop. For example, in the above, we could easily add (at least) two more runtime checks: same_upper_items: (Result and lower <= upper) implies item( upper ) = other.item(upper) same_lower_items: (Result and lower <= upper) implies item( lower ) = other.item(lower) Of course these are redundant with "same_elements" but provide the same kind of extra security that "same_bounds" provides, so why not include them as well? Where do we stop? My solution, of course, was to stop adding redundant checks before I started :-). > > Best regards, > > -- BM Best, -- Jim > > ================================================== > > End of NICE-ESG-Libs Digest > ****************************** >
