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, 14 Dec 95 09:57:26 PST From: bertrand@eiffel.com (Bertrand Meyer) Subject: Postcondition of is_equal To: NICE-ESG-Libs@atlanta.twr.com From Jim (I think): > 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. I agree with this EXCEPT for the comment line marked !!!, which should be removed: (1) It is not the role of a standard to apologize. (2) Although we strive to avoid redundant assertions, there is no absolute rule that the set of assertions should be minimal. -- BM
