Re: [eiffel-nice-library] COMPARABLE finel (?), minor changes.
generally I'm impressed by your sharp eye!
On 30 Sep 2002, at 12:52, Eric Bezault wrote:
> > max (other: like Current): like Current
> > -- The greater of current object and other, implementers choice
> > -- if they are equal
> > require
> > other_exists: other /= Void
> > ensure
> > current_or_other: (Result = Current) or (Result = other)
> > at_least_current: (Result = Current) or (Current < Result)
> > at_least_other: (Result = other) or (other < Result)
> Consider that:
> other /= Current
> other.is_equal (Current)
> Therefore Result is either 'other' or 'Current' (implementers choice).
> Consider that it's 'Current'. The postcondition 'at_least_other' says
> that 'other < Result' (because 'Result /= other'). But 'Result = Current',
> so we have 'other < Current'. This violates our assumption that
> 'other.is_equal (Current)'. Or did a miss something?
current_or_other: (Result = Current) or (Result = other)
result_is_other: Current < other implies Result = other
result_is_current: other < Current implies Result = Current
Alternatively I was thinking about a variant of postcondition #1:
Result /= Current implies Result = other