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.) Best regards, -- BM
