Loading ...
Sorry, an error occurred while loading the content.

Re: [eiffel-nice-library] COMPARABLE finel (?), minor changes.

Expand Messages
  • Ulrich Windl
    Eric, generally I m impressed by your sharp eye! On 30 Sep 2002, at 12:52, Eric Bezault wrote: [...] ... What about: current_or_other: (Result = Current) or
    Message 1 of 4 , Sep 30, 2002
    • 0 Attachment
      Eric,

      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?

      What about:
      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

      Regards,
      ulrich
    Your message has been successfully submitted and would be delivered to recipients shortly.