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

COMPARABLE next iteration

Expand Messages
  • Arno Wagner
    ... Yes, same here. The last 3 weeks where crazy (start of the lectures and the flu going round). As to Eric s comments: O.K., I have corrected the header and
    Message 1 of 2 , Oct 22, 2002
    • 0 Attachment
      Eric Bezault wrote:

      > Sorry for not reviewing class COMPARABLE before. You know what
      > it is: lack of time, etc.

      Yes, same here. The last 3 weeks where crazy (start of the
      lectures and the flu going round).

      As to Eric's comments:

      O.K., I have corrected the header and replaced all the
      "other_exists" with "other_not_void".

      I am not aware of the status on ANY vs. ANY/GENERAL. Does
      anybody know what it is and can give me a pointer?

      As to "same_type: Result implies same_type (other)" for
      "is_equal". O.k. I have added that, although it is completely
      redundant. There is what I fear is a serious bug in Eiffel.
      It manifests itself in the postcondition "symmetric" of
      "is_equal" actually specifying a run-time type constraint.
      If you call "is_equal" with something of not "same_type"
      you get a run-time type violation. Very bad.
      This might also be the reason why at least SE does not
      have the postcondition "symmetric" on "is_equal".
      I think it was while thinking about this that I threw
      out the postcondition 'same_type'....

      I am not quite sure about the way to tackle this, but
      it is obviously not what was intended by feature "is_equal".
      As I suspect all the vendors for now ignore the postcondition
      "symmetric", I propose to just live with the problem for now
      and add "revision of ANY/General" to the end of the TODO-list.
      The changes made there should then propagate automatically
      to all the classes redefining 'is_equal'. However if there
      is a desire to tackle this problem now, we can also make it
      the next topic.

      for "max":
      > > 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?

      Indeed. So the "at_least..." postconditions will have to
      change. Ulrich proposed

      current_or_other: (Result = Current) or (Result = other)
      result_is_other: Current < other implies Result = other
      result_is_current: other < Current implies Result = Current

      which I like and have added.

      For the indention of the invariant, I do not really care.
      I have attempted some beautification, but if anybody sees
      a better way, please tell me.

      As for looking at STRING now, I would propose to deferr that to
      the next iteration. Since the functionality here does not change
      (or gets more general in the case of three_way_comparison), I
      expect there will be no problems.

      Comments? Questions? Proposals?

      Arno

      ----------------------------------------------------------------------

      indexing

      description: "Objects of this type are ordered with respect %
      %to a total order relation."
      Note: "The basic operation `<' is is used to define all other %
      %operations. `is_equal' is redefined in terms of `<'."

      deferred class interface

      feature -- Basic Specifiers

      infix "<" (other: like Current): BOOLEAN
      -- Is current object less than other?
      require
      other_not_void: other /= Void

      feature -- Comparison

      infix "<=" (other: like Current): BOOLEAN
      -- Is current object less than or equal to `other'?
      require
      other_not_void: other /= Void
      ensure
      definition: Result = not (other < Current)


      infix ">=" (other: like Current): BOOLEAN
      -- Is current object greater than or equal to `other'?
      require
      other_not_void: other /= Void
      ensure
      definition: Result = not (Current < other)


      infix ">" (other: like Current): BOOLEAN
      -- Is current object greater than `other'?
      require
      other_not_void: other /= Void
      ensure
      definition: Result = (other < Current)


      is_equal (other: like Current): BOOLEAN
      -- Is `other' attached to an object considered equal
      -- to current object?
      -- (Redefined from GENERAL.)
      require
      other_not_void: other /= Void
      ensure
      definition: Result = (not (Current < other) and
      not (other < Current))
      symmetric: Result implies other.is_equal (Current);
      consistent: standard_is_equal (other) implies Result;
      same_type: Result implies same_type (other)

      three_way_comparison (other: like Current): INTEGER)
      -- If current object equal to `other', 0; if smaller,
      -- -1; if greater, 1.
      -- Redundant postcondition included for clarity.
      require
      other_not_void: other /= Void
      ensure
      legal_result: Result = -1 or Result = 0 or Result = 1
      zero_on_equal: (Result = 0) =
      (not (Current < other) and not (other < Current))
      positive_on_larger: (Result = 1) = (other < Current)
      negative_on_smaller: (Result = -1) = (Current < other)

      feature -- Selection

      max (other: like Current): like Current
      -- The greater of current object and `other', implementers choice
      -- if they are equal.
      require
      other_not_void: other /= Void
      ensure
      current_or_other: (Result = Current) or (Result = other)
      result_is_other: Current < other implies Result = other
      result_is_current: other < Current implies Result = Current

      min (other: like Current): like Current
      -- The smaller of current object and `other', implementers choice
      -- if they are equal.
      require
      other_not_void: other /= Void
      ensure
      current_or_other: (Result = Current) or (Result = other)
      result_is_other: other < Current implies Result = other
      result_is_current: Current < other implies Result = Current


      invariant

      irreflexivity: not (Current < Current)

      -- asymmetry: for_all other : like Current :
      -- ((other < Current) implies not (Current < other))

      -- transitivity: for_all second : like Current :
      -- for all third : like Current :
      -- ((second < Current) and (Current < third) implies (second < third)

      -- trichotomy: for_all other : like Current :
      -- exactly_one_of(other < Current, Current < other, is_equal(other))

      end

      --
      Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@...
      GnuPG: ID: 1E25338F FP: 0C30 5782 9D93 F785 E79C 0296 797F 6B50 1E25 338F
      ----
      For every complex problem there is an answer that is clear, simple,
      and wrong. -- H L Mencken
    • Eric Bezault
      ... Two is . ... The class name is missing here. ... -- Eric Bezault mailto:ericb@gobosoft.com http://www.gobosoft.com
      Message 2 of 2 , Oct 22, 2002
      • 0 Attachment
        Arno Wagner wrote:
        >
        > indexing
        >
        > description: "Objects of this type are ordered with respect %
        > %to a total order relation."
        > Note: "The basic operation `<' is is used to define all other %
        -------------------------------------^^^^^^
        Two 'is'.

        > %operations. `is_equal' is redefined in terms of `<'."
        >
        > deferred class interface
        >

        The class name is missing here.

        > feature -- Basic Specifiers

        --
        Eric Bezault
        mailto:ericb@...
        http://www.gobosoft.com

        ___________________________________________________________________
        Haut D�bit: Modem offert soit 150,92 euros rembours�s sur le Pack eXtense de Wanadoo !
        Profitez du Haut D�bit � partir de 30 euros/mois : http://www.ifrance.com/_reloc/w
      Your message has been successfully submitted and would be delivered to recipients shortly.