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

|
|