NICE-ESG-Libs Digest        Tue, 12 Dec 95       Volume 1 : Issue 315 

Today's Topics:
      Proposal RB-3: Amend 'is_equal' postcondition 'definition'


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 02:24:56 +0000 From: Roger Browne Subject: Proposal RB-3: Amend 'is_equal' postcondition 'definition' To: NICE-ESG-Libs@atlanta.twr.com This proposal aims to correct a minor error with the 'definition' postcondition of 'is_equal'. I have discussed this proposed amendment with James McKim and he is happy with this fix. Regards, Roger ===== Tag: RB-3: Amend 'is_equal' postcondition 'definition' Class: ARRAY Proposed Change: Amend proposal RB-2 (James McKim's ARRAY class) to change the postcondition of 'is_equal'. Details: Amend proposal RB-2 to replace this postcondition to 'is_equal'... ensure definition: Result = (lower = other.lower) and (upper = other.upper) --and for_all i, lower..upper (item(i) = other.item(i)) ...by this postcondition... ensure definition: -- Result = (lower = other.lower) and (upper = other.upper) and for_all i, lower..upper (item(i) = other.item(i)) Rationale: The existing postcondition is correct if considered in its entirety. However, when the non-executable part is commented out, the remaining subexpression does not yield a meaningful result when evaluated. Migration strategy: There is no effect on existing code. -- -- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525 -- Everything Eiffel: compilers/libraries/publications | +44-1772-687525