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

Possible changes to COMPARABLE

Expand Messages
  • Arno Wagner
    Here is an initial proposal for COMPARABLE. I think we can discuss this in one step, and vote on it in a block doing the different issues in separate votes,
    Message 1 of 9 , Aug 6, 2002
    • 0 Attachment
      Here is an initial proposal for COMPARABLE.

      I think we can discuss this in one step, and vote on it
      in a block doing the different issues in separate votes,
      but at the same time or in rapid succession.

      Points I see:

      The name is misleading. What is modelled is a total
      order. In mathematical terms "comparable" would
      mean that there is an equality operator defined on a set,
      not an order. Usually these exist and are total. The same
      is true in Eiffel, look at feature "equal" to find it.

      So COMPARABLE should really be named TOTALLY_ORDERED.
      I am not proposing to change the name, but to change the
      head comment. ELKS95 says

      "Objects that may be compared according to a total order relation";
      note: "The basic operation is `<` (less than); others are defined
      in terms of this operation and `is_equal'."

      I do not like the "may". It confuses things. My proposal:

      "Objects of this type are ordered with respect to a total
      order relation `<'. This basic operation is used together
      with `is_equal' to define additional operators."

      Furthermore I propose the following changes:

      - Remove the invariant and put it in a postcondition
      'strict' in '<'. Furthermore add a postcondition
      'total' to '<'.
      The advantage is that 'is_equal' need not be redefined
      anymore as trichotomy is now defined in the contract of "<".
      This is good as trichotomy is really a property of '<' that
      is defined in relation to a given definition for 'is_equal'.
      It is _not_ a constraint on 'is_equal'!

      Affected: Features "<", 'is_equal'
      Invariant 'irreflexive_comparison'

      - 'min','max' are over-specified: When the elements are equal via
      'is_equal' there is a preference for a specific result
      (Current). The way I read the specification of 'is_equal' in
      GENERAL is that a redefinition of 'is_equal' that has different
      objects being equal is entirely permissible, as long as equality
      implies same type and 'standard_is_equal' implies 'is_equal'. The
      most general implementation would give 'is_equal' the same
      semantics as 'same_type'.

      I hope I got this right. Please correct me if not!

      Change: Allow 'min', 'max' to return any argument
      if arguments are equal via 'is_equal'.

      Affected: Postconditions of features 'min', 'max'.


      That seems to be it. If I missed something, please speak up!

      Here is the rest of COMPARABLE from ELKS95. Places where I
      think changes are needed are marked with '#' and a comment
      behind it. The changes I propose are the following:

      -----

      feature -- Comparison
      infix "<" (other: like Current): BOOLEAN
      -- Is current object less than other?
      require
      other_exists: other /= Void
      ensure
      asymmetric: Result implies not (other < Current)
      # Add the following:
      #
      # strict: Result implies not Current.is_equal(other)
      # total: not Current.is_equal(other) implies
      # (Current < other or other < Current)
      #
      # This is in part covered by the invariant, but I feel it is needed
      # here, and here only. I propose to remove the invariant.


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


      infix ">=" (other: like Current): BOOLEAN
      -- Is current object greater than or equal to other?
      require
      other_exists: other /= Void
      ensure
      definition: Result = (other <= Current)
      # Replace this with
      #
      # definition: Result = (other < Current) or is_equal (other)
      #
      # in order to get a direct dependency on the basic operations.


      infix ">" (other: like Current): BOOLEAN
      -- Is current object greater than other?
      require
      other_exists: 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
      symmetric: Result implies other.is_equal (Current);
      consistent: standard_is_equal (other) implies Result;
      trichotomy: Result = (not (Current < other) and not (other < Current))
      #
      # 'trichotomy' is redundant with the postcondition 'strict' on '<' and
      # 'definition' on '>'. We could remove it and do without redefinition
      # of 'is_equal' entirely. My personal feeling is that this would be the way
      # to go: An order relation has to respect the already defined equality
      # relation, _without_ putting any additional constraints on it.
      # 'consistent' and 'symmetric' are already in GENERAL.
      #



      max (other: like Current): like Current
      -- The greater of current object and other
      require
      other_exists: other /= Void
      ensure
      current_if_not_smaller: (Current >= other) implies (Result = Current)
      other_if_smaller: (Current < other) implies (Result = other)
      # This is too strict. If some objects change is_equal so that some
      # different objects cannot be distinguished by 'is_equal' anymore
      # this postcondition mandates that the result has to be 'Current'.
      # There is no need for that.
      # I would propose to replace the entire postcondition with
      #
      # definition: Result >= Current and Result >= other and
      # (Result = Current or Result = other)
      #
      # neatly removing the problem.



      min (other: like Current): like Current
      -- The smaller of current object and other
      require
      other_exists: other /= Void
      ensure
      current_if_not_greater: (Current <= other) implies (Result = Current)
      other_if_greater: (Current > other) implies (Result = other)
      # Same thing as with 'max'. I propose to change the postcondition to
      #
      # definition: Result <= Current and Result <= other and
      # (Result = Current or Result = other)
      #


      three_way_comparison (other: like Current): INTEGER)
      -- If current object equal to other, 0; if smaller,
      -- -1; if greater, 1.
      require
      other_exists: other /= Void
      ensure
      equal_zero: (Result = 0) = is_equal (other);
      smaller_negative: (Result = -1) = (Current < other);
      greater_positive: (Result = 1) = (Current > other)

      invariant

      irreflexive_comparison: not (Current < Current)
      # I propose to remove this invariant. The postcondition 'strict' at
      # feature '<' is entirely enough and is in the place where it belongs.

      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
    • Ulrich Windl
      ... Hmm, ugly: What about TOTALLY_ORDERABLE? it s deferred after all. (To non-methematicans COMPARE possibly means something like smaller or larger, maybe
      Message 2 of 9 , Aug 6, 2002
      • 0 Attachment
        On 6 Aug 2002, at 13:01, Arno Wagner wrote:

        > Here is an initial proposal for COMPARABLE.
        >
        > I think we can discuss this in one step, and vote on it
        > in a block doing the different issues in separate votes,
        > but at the same time or in rapid succession.
        >
        > Points I see:
        >
        > The name is misleading. What is modelled is a total
        > order. In mathematical terms "comparable" would
        > mean that there is an equality operator defined on a set,
        > not an order. Usually these exist and are total. The same
        > is true in Eiffel, look at feature "equal" to find it.
        >
        > So COMPARABLE should really be named TOTALLY_ORDERED.

        Hmm, ugly: What about TOTALLY_ORDERABLE? it's deferred after all.
        (To non-methematicans COMPARE possibly means something like smaller or
        larger, maybe that's why the original name was COMPARABLE).

        > I am not proposing to change the name, but to change the
        > head comment. ELKS95 says
        >
        > "Objects that may be compared according to a total order relation";
        > note: "The basic operation is `<` (less than); others are defined
        > in terms of this operation and `is_equal'."

        should "is_less_than" be declared as synonym for "<"? It would match
        nicely with "is_equal"...

        >
        > I do not like the "may". It confuses things. My proposal:
        >
        > "Objects of this type are ordered with respect to a total
        > order relation `<'. This basic operation is used together
        > with `is_equal' to define additional operators."

        Talking about objects of deferred classes is also not very good: What
        about "Total order using `<' and `is_equal' as relational operators".
        Is it too crisp?

        >
        > Furthermore I propose the following changes:
        >
        > - Remove the invariant and put it in a postcondition
        > 'strict' in '<'. Furthermore add a postcondition
        > 'total' to '<'.
        > The advantage is that 'is_equal' need not be redefined
        > anymore as trichotomy is now defined in the contract of "<".
        > This is good as trichotomy is really a property of '<' that
        > is defined in relation to a given definition for 'is_equal'.
        > It is _not_ a constraint on 'is_equal'!

        Maybe for the future: Quote the invariants and post conditions you are
        talking about.

        >
        > Affected: Features "<", 'is_equal'
        > Invariant 'irreflexive_comparison'
        >
        > - 'min','max' are over-specified: When the elements are equal via
        > 'is_equal' there is a preference for a specific result
        > (Current). The way I read the specification of 'is_equal' in
        > GENERAL is that a redefinition of 'is_equal' that has different
        > objects being equal is entirely permissible, as long as equality
        > implies same type and 'standard_is_equal' implies 'is_equal'. The
        > most general implementation would give 'is_equal' the same
        > semantics as 'same_type'.
        >
        > I hope I got this right. Please correct me if not!
        >
        > Change: Allow 'min', 'max' to return any argument
        > if arguments are equal via 'is_equal'.
        >
        > Affected: Postconditions of features 'min', 'max'.
        >
        >
        > That seems to be it. If I missed something, please speak up!
        >
        > Here is the rest of COMPARABLE from ELKS95. Places where I
        > think changes are needed are marked with '#' and a comment
        > behind it. The changes I propose are the following:
        >
        > -----
        >
        > feature -- Comparison
        > infix "<" (other: like Current): BOOLEAN
        > -- Is current object less than other?
        > require
        > other_exists: other /= Void
        > ensure
        > asymmetric: Result implies not (other < Current)
        > # Add the following:
        > #
        > # strict: Result implies not Current.is_equal(other)

        Maybe replace "strict" with "strict_ordering" (or similar).

        > # total: not Current.is_equal(other) implies
        > # (Current < other or other < Current)
        > #

        (same for "total")

        > # This is in part covered by the invariant, but I feel it is needed
        > # here, and here only. I propose to remove the invariant.
        >
        >
        > infix "<=" (other: like Current): BOOLEAN
        > -- Is current object less than or equal to other?
        > require
        > other_exists: other /= Void
        > ensure
        > definition: Result = (Current < other) or is_equal (other)
        >
        >
        > infix ">=" (other: like Current): BOOLEAN
        > -- Is current object greater than or equal to other?
        > require
        > other_exists: other /= Void
        > ensure
        > definition: Result = (other <= Current)
        > # Replace this with
        > #
        > # definition: Result = (other < Current) or is_equal (other)
        > #
        > # in order to get a direct dependency on the basic operations.

        I see little advantage here.

        >
        >
        > infix ">" (other: like Current): BOOLEAN
        > -- Is current object greater than other?
        > require
        > other_exists: 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
        > symmetric: Result implies other.is_equal (Current);
        > consistent: standard_is_equal (other) implies Result;
        > trichotomy: Result = (not (Current < other) and not (other < Current))

        The outermost pair of parentheses adds nothing to readability IMHO

        > #
        > # 'trichotomy' is redundant with the postcondition 'strict' on '<' and
        > # 'definition' on '>'. We could remove it and do without redefinition
        > # of 'is_equal' entirely. My personal feeling is that this would be the way
        > # to go: An order relation has to respect the already defined equality
        > # relation, _without_ putting any additional constraints on it.
        > # 'consistent' and 'symmetric' are already in GENERAL.
        > #
        >
        >
        >
        > max (other: like Current): like Current
        > -- The greater of current object and other
        > require
        > other_exists: other /= Void
        > ensure
        > current_if_not_smaller: (Current >= other) implies (Result = Current)
        > other_if_smaller: (Current < other) implies (Result = other)
        > # This is too strict. If some objects change is_equal so that some
        > # different objects cannot be distinguished by 'is_equal' anymore
        > # this postcondition mandates that the result has to be 'Current'.
        > # There is no need for that.

        Maybe if you use it implementing "stable sort algorithms" it could be
        interesting.

        > # I would propose to replace the entire postcondition with
        > #
        > # definition: Result >= Current and Result >= other and
        > # (Result = Current or Result = other)
        > #
        > # neatly removing the problem.
        >
        >
        >
        > min (other: like Current): like Current
        > -- The smaller of current object and other
        > require
        > other_exists: other /= Void
        > ensure
        > current_if_not_greater: (Current <= other) implies (Result = Current)
        > other_if_greater: (Current > other) implies (Result = other)
        > # Same thing as with 'max'. I propose to change the postcondition to
        > #
        > # definition: Result <= Current and Result <= other and
        > # (Result = Current or Result = other)
        > #
        >
        >
        > three_way_comparison (other: like Current): INTEGER)
        > -- If current object equal to other, 0; if smaller,
        > -- -1; if greater, 1.
        > require
        > other_exists: other /= Void
        > ensure
        > equal_zero: (Result = 0) = is_equal (other);
        > smaller_negative: (Result = -1) = (Current < other);
        > greater_positive: (Result = 1) = (Current > other)

        Hmm.

        zero_if_equal: is_equal(other) implies Result = 0
        negative_if_smaller: Current < other implies Result = -1
        positive_if_larger: Current > other implies Result = 1

        ??? What about that the left sides should have empty intersections

        >
        > invariant
        >
        > irreflexive_comparison: not (Current < Current)
        > # I propose to remove this invariant. The postcondition 'strict' at
        > # feature '<' is entirely enough and is in the place where it belongs.
        >
        > end
        >

        Regards,
        Ulrich
      • Christian Couder
        Hi all ! ... Why not : current_or_other: Result = Current or Result = other at_least_current: Result = Current at_least_other: Result = other Isn t it better
        Message 3 of 9 , Aug 6, 2002
        • 0 Attachment
          Hi all !

          On Tuesday 06 August 2002 13:01, Arno Wagner wrote:
          >
          > max (other: like Current): like Current
          > -- The greater of current object and other
          > require
          > other_exists: other /= Void
          > ensure
          > current_if_not_smaller: (Current >= other) implies (Result =
          > Current) other_if_smaller: (Current < other) implies (Result = other) #
          > This is too strict. If some objects change is_equal so that some #
          > different objects cannot be distinguished by 'is_equal' anymore
          > # this postcondition mandates that the result has to be 'Current'.
          > # There is no need for that.
          > # I would propose to replace the entire postcondition with
          > #
          > # definition: Result >= Current and Result >= other and
          > # (Result = Current or Result = other)
          > #
          > # neatly removing the problem.

          Why not :

          current_or_other: Result = Current or Result = other
          at_least_current: Result >= Current
          at_least_other: Result >= other

          Isn't it better when the conditions are splited as mus as possible ?

          > min (other: like Current): like Current
          > -- The smaller of current object and other
          > require
          > other_exists: other /= Void
          > ensure
          > current_if_not_greater: (Current <= other) implies (Result =
          > Current) other_if_greater: (Current > other) implies (Result = other) #
          > Same thing as with 'max'. I propose to change the postcondition to #
          > # definition: Result <= Current and Result <= other and
          > # (Result = Current or Result = other)
          > #

          As above :

          current_or_other: Result = Current or Result = other
          at_most_current: Result <= Current
          at_most_other: Result <= other

          Regards,
          Christian.
        • Arno Wagner
          ... Indeed. I like this proposal. [ same for min spipped] Rgerads, Arno -- Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@tik.ee.ethz.ch
          Message 4 of 9 , Aug 6, 2002
          • 0 Attachment
            On Tue, Aug 06, 2002 at 08:28:46PM +0200, Christian Couder wrote:
            > Hi all !
            >
            > On Tuesday 06 August 2002 13:01, Arno Wagner wrote:
            > >
            > > max (other: like Current): like Current
            > > -- The greater of current object and other
            > > require
            > > other_exists: other /= Void
            > > ensure
            > > current_if_not_smaller: (Current >= other) implies (Result =
            > > Current) other_if_smaller: (Current < other) implies (Result = other) #
            > > This is too strict. If some objects change is_equal so that some #
            > > different objects cannot be distinguished by 'is_equal' anymore
            > > # this postcondition mandates that the result has to be 'Current'.
            > > # There is no need for that.
            > > # I would propose to replace the entire postcondition with
            > > #
            > > # definition: Result >= Current and Result >= other and
            > > # (Result = Current or Result = other)
            > > #
            > > # neatly removing the problem.
            >
            > Why not :
            >
            > current_or_other: Result = Current or Result = other
            > at_least_current: Result >= Current
            > at_least_other: Result >= other
            >
            > Isn't it better when the conditions are splited as mus as possible ?

            Indeed. I like this proposal.

            [ same for 'min' spipped]

            Rgerads,
            Arno


            --
            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
          • Alexander Kogtenkov
            ... Cannot it be simplified to # strict: Result implies not is_equal (other) # total: not is_equal (other) implies # (Result or
            Message 5 of 9 , Aug 7, 2002
            • 0 Attachment
              Arno Wagner wrote:

              > feature -- Comparison
              > infix "<" (other: like Current): BOOLEAN
              > -- Is current object less than other?
              > require
              > other_exists: other /= Void
              > ensure
              > asymmetric: Result implies not (other < Current)
              > # Add the following:
              > #
              > # strict: Result implies not Current.is_equal(other)
              > # total: not Current.is_equal(other) implies
              > # (Current < other or other < Current)
              > #
              > # This is in part covered by the invariant, but I feel it is needed
              > # here, and here only. I propose to remove the invariant.

              Cannot it be simplified to

              # strict: Result implies not is_equal (other)
              # total: not is_equal (other) implies
              # (Result or other < Current)

              ?

              > infix "<=" (other: like Current): BOOLEAN
              > -- Is current object less than or equal to other?
              > require
              > other_exists: other /= Void
              > ensure
              > definition: Result = (Current < other) or is_equal (other)

              Should not it be

              definition: Result = ((Current < other) or is_equal (other))

              ?

              > infix ">=" (other: like Current): BOOLEAN
              > -- Is current object greater than or equal to other?
              > require
              > other_exists: other /= Void
              > ensure
              > definition: Result = (other <= Current)
              > # Replace this with
              > #
              > # definition: Result = (other < Current) or is_equal (other)
              > #
              > # in order to get a direct dependency on the basic operations.

              The same here.

              Regards,
              Alexander Kogtenkov
              Object Tools, Moscow
            • Alexander Kogtenkov
              ... It makes sure that the expression is considered properly. Without parentheses it would be interpreted as trichotomy: (Result = not (Current
              Message 6 of 9 , Aug 7, 2002
              • 0 Attachment
                Ulrich Windl wrote:

                > > 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
                > > symmetric: Result implies other.is_equal (Current);
                > > consistent: standard_is_equal (other) implies Result;
                > > trichotomy: Result = (not (Current < other) and not (other < Current))
                >
                > The outermost pair of parentheses adds nothing to readability IMHO

                It makes sure that the expression is considered properly.
                Without parentheses it would be interpreted as

                trichotomy: (Result = not (Current < other)) and not (other < Current)

                Regards,
                Alexander Kogtenkov
                Object Tools, Moscow
              • Arno Wagner
                ... Yes it can. I don t mind either way. The first is more explicit, the second one more compact. Both do the job. ... Indeed. I keep forgetting that. Regards,
                Message 7 of 9 , Aug 7, 2002
                • 0 Attachment
                  On Wed, Aug 07, 2002 at 01:46:34PM +0400, Alexander Kogtenkov wrote:
                  > Arno Wagner wrote:
                  >
                  > > feature -- Comparison
                  > > infix "<" (other: like Current): BOOLEAN
                  > > -- Is current object less than other?
                  > > require
                  > > other_exists: other /= Void
                  > > ensure
                  > > asymmetric: Result implies not (other < Current)
                  > > # Add the following:
                  > > #
                  > > # strict: Result implies not Current.is_equal(other)
                  > > # total: not Current.is_equal(other) implies
                  > > # (Current < other or other < Current)
                  > > #
                  > > # This is in part covered by the invariant, but I feel it is needed
                  > > # here, and here only. I propose to remove the invariant.
                  >
                  > Cannot it be simplified to
                  >
                  > # strict: Result implies not is_equal (other)
                  > # total: not is_equal (other) implies
                  > # (Result or other < Current)
                  >
                  > ?

                  Yes it can. I don't mind either way. The first is
                  more explicit, the second one more compact. Both
                  do the job.

                  > > infix "<=" (other: like Current): BOOLEAN
                  > > -- Is current object less than or equal to other?
                  > > require
                  > > other_exists: other /= Void
                  > > ensure
                  > > definition: Result = (Current < other) or is_equal (other)
                  >
                  > Should not it be
                  >
                  > definition: Result = ((Current < other) or is_equal (other))
                  >
                  > ?

                  Indeed. I keep forgetting that.

                  Regards,
                  Arno

                  --
                  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
                • James McKim
                  Hey Arno, Thanks for taking the lead, both for the group in general and for COMPARABLE in particular. I m sure you ll do a great job! More below. ... I like
                  Message 8 of 9 , Aug 9, 2002
                  • 0 Attachment
                    Hey Arno,

                    Thanks for taking the lead, both for the group in
                    general and for COMPARABLE in particular. I'm sure
                    you'll do a great job!

                    More below.

                    Arno Wagner wrote:

                    >
                    > Here is an initial proposal for COMPARABLE.
                    >
                    > I think we can discuss this in one step, and vote on it
                    > in a block doing the different issues in separate votes,
                    > but at the same time or in rapid succession.
                    >
                    > Points I see:
                    >
                    > The name is misleading. What is modelled is a total
                    > order. In mathematical terms "comparable" would
                    > mean that there is an equality operator defined on a set,
                    > not an order. Usually these exist and are total. The same
                    > is true in Eiffel, look at feature "equal" to find it.
                    >
                    > So COMPARABLE should really be named TOTALLY_ORDERED.
                    > I am not proposing to change the name, but to change the
                    > head comment. ELKS95 says
                    >
                    > "Objects that may be compared according to a total order relation";
                    > note: "The basic operation is `<` (less than); others are defined
                    > in terms of this operation and `is_equal'."
                    >
                    > I do not like the "may". It confuses things. My proposal:
                    >
                    > "Objects of this type are ordered with respect to a total
                    > order relation `<'. This basic operation is used together
                    > with `is_equal' to define additional operators."

                    I like this change, but note that actually we can do it
                    entirely in terms of `<' as the basic specifier for
                    COMPARABLE.

                    >
                    > Furthermore I propose the following changes:
                    >
                    > - Remove the invariant and put it in a postcondition
                    > 'strict' in '<'. Furthermore add a postcondition
                    > 'total' to '<'.
                    > The advantage is that 'is_equal' need not be redefined
                    > anymore as trichotomy is now defined in the contract of "<".
                    > This is good as trichotomy is really a property of '<' that
                    > is defined in relation to a given definition for 'is_equal'.
                    > It is _not_ a constraint on 'is_equal'!
                    >
                    > Affected: Features "<", 'is_equal'
                    > Invariant 'irreflexive_comparison'

                    I see the point, but I disagree. 'is_equal' will have
                    to be redefined anyway in all but trivial cases as
                    exemplified by STRING and ARRAY. Might as well be up
                    front about it. Besides the whole idea of the disciplined
                    approach we're using is to identify a few (in this
                    case one) basic specifiers and define everything else
                    in terms of them. Ideally the basic specifiers themselves
                    have no postconditions.

                    So I'd prefer this back the other way. It may well
                    be, however, that 'trichotomy' is not the best label
                    for the clause in the postcondition of 'is_equal'.

                    The deeper and harder problem here is whether 'is_equal'
                    is the right version of equality to play a role in
                    in the total ordering. Those extra postconditions make
                    this somewhat problematic. If is_equal returns False
                    only because of type mismatch, which of < and > will
                    be true?

                    >
                    > - 'min','max' are over-specified: When the elements are equal via
                    > 'is_equal' there is a preference for a specific result
                    > (Current). The way I read the specification of 'is_equal' in
                    > GENERAL is that a redefinition of 'is_equal' that has different
                    > objects being equal is entirely permissible, as long as equality
                    > implies same type and 'standard_is_equal' implies 'is_equal'. The
                    > most general implementation would give 'is_equal' the same
                    > semantics as 'same_type'.
                    >
                    > I hope I got this right. Please correct me if not!
                    >
                    > Change: Allow 'min', 'max' to return any argument
                    > if arguments are equal via 'is_equal'.
                    >
                    > Affected: Postconditions of features 'min', 'max'.

                    Interesting. I don't have any problem letting the implementer
                    decide which of Current or other to return. Although if
                    we do that I think we should somehow mark the spec as
                    indeterminate in this case.

                    But I'm not sure of the reasoning. If 'is_equal' is
                    redefined to mean 'same_type' (or any other redefinition)
                    why would you then prefer to return 'other' as the max?.
                    Perhaps an example would help?

                    >
                    >
                    > That seems to be it. If I missed something, please speak up!
                    >
                    > Here is the rest of COMPARABLE from ELKS95. Places where I
                    > think changes are needed are marked with '#' and a comment
                    > behind it. The changes I propose are the following:

                    Nice job putting all this together! Still more below.

                    >
                    > -----
                    >
                    > feature -- Comparison
                    > infix "<" (other: like Current): BOOLEAN
                    > -- Is current object less than other?
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > asymmetric: Result implies not (other < Current)
                    > # Add the following:
                    > #
                    > # strict: Result implies not Current.is_equal(other)
                    > # total: not Current.is_equal(other) implies
                    > # (Current < other or other < Current)
                    > #
                    > # This is in part covered by the invariant, but I feel it is needed
                    > # here, and here only. I propose to remove the invariant.

                    As noted above, I'd put this back the way it was before, no
                    postconditions.

                    >
                    >
                    > infix "<=" (other: like Current): BOOLEAN
                    > -- Is current object less than or equal to other?
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > definition: Result = (Current < other) or is_equal (other)

                    I'd prefer Result = not (other < Current)

                    Keep every definition strictly in terms of <. Well at
                    least all the simple ones. We may have to vary from
                    this when we hit max, min, three_way.

                    >
                    >
                    > infix ">=" (other: like Current): BOOLEAN
                    > -- Is current object greater than or equal to other?
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > definition: Result = (other <= Current)
                    > # Replace this with
                    > #
                    > # definition: Result = (other < Current) or is_equal (other)
                    > #
                    > # in order to get a direct dependency on the basic operations.

                    Result = not (Current < other)

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

                    Good.

                    >
                    >
                    > 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
                    > symmetric: Result implies other.is_equal (Current);
                    > consistent: standard_is_equal (other) implies Result;
                    > trichotomy: Result = (not (Current < other) and not (other < Current))
                    > #
                    > # 'trichotomy' is redundant with the postcondition 'strict' on '<' and
                    > # 'definition' on '>'. We could remove it and do without redefinition
                    > # of 'is_equal' entirely. My personal feeling is that this would be the way
                    > # to go: An order relation has to respect the already defined equality
                    > # relation, _without_ putting any additional constraints on it.
                    > # 'consistent' and 'symmetric' are already in GENERAL.
                    > #

                    Again, I would keep this as it was, see above for reasoning.
                    'definition' might be a better name than 'trichotomy'.

                    >
                    >
                    >
                    > max (other: like Current): like Current
                    > -- The greater of current object and other
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > current_if_not_smaller: (Current >= other) implies (Result = Current)

                    Hmmm... Could be not (Current < other) implies (Result = Current)

                    > other_if_smaller: (Current < other) implies (Result = other)
                    > # This is too strict. If some objects change is_equal so that some
                    > # different objects cannot be distinguished by 'is_equal' anymore
                    > # this postcondition mandates that the result has to be 'Current'.
                    > # There is no need for that.
                    > # I would propose to replace the entire postcondition with
                    > #
                    > # definition: Result >= Current and Result >= other and
                    > # (Result = Current or Result = other)
                    > #
                    > # neatly removing the problem.

                    No objection in principle, but again I'm not sure it's a useful
                    change....

                    >
                    >
                    >
                    > min (other: like Current): like Current
                    > -- The smaller of current object and other
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > current_if_not_greater: (Current <= other) implies (Result = Current)
                    > other_if_greater: (Current > other) implies (Result = other)

                    (other < Current) implies....

                    > # Same thing as with 'max'. I propose to change the postcondition to
                    > #
                    > # definition: Result <= Current and Result <= other and
                    > # (Result = Current or Result = other)
                    > #

                    Ditto.

                    >
                    >
                    > three_way_comparison (other: like Current): INTEGER)
                    > -- If current object equal to other, 0; if smaller,
                    > -- -1; if greater, 1.
                    > require
                    > other_exists: other /= Void
                    > ensure
                    > equal_zero: (Result = 0) = is_equal (other);
                    > smaller_negative: (Result = -1) = (Current < other);
                    > greater_positive: (Result = 1) = (Current > other)

                    For the last one perhaps (Result = 1) = (other < Current)

                    That way _everything_ is defined in terms of < except the
                    one clause equal_zero immediately above. And I don't see
                    a way to fix that one without really damaging readability.

                    >
                    > invariant
                    >
                    > irreflexive_comparison: not (Current < Current)
                    > # I propose to remove this invariant. The postcondition 'strict' at
                    > # feature '<' is entirely enough and is in the place where it belongs.

                    Well, most invariants are redundant. Again see STRING and ARRAY. The
                    idea is to provide summary information to confirm the abstraction,
                    in this case a total ordering. I'd actually like to see more. E.g.

                    reflexive_comparison: Current <= Current (there's probably a
                    better name.)

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

                    -- antisymmetry: for_all other : like Current
                    -- ((other <= Current) and (Current <= other) implies is_equal(other))

                    -- trichotomy: for_all other : like Current
                    -- ((other < Current) or (Current < other) or is_equal(other))

                    Again there may be better names. Indeed to get full trichotomy
                    you'd need to specify that just one of the three is true.
                    And they're not compilable, but again they confirm the fact that
                    we're really specifying a total ordering.

                    Arno, Michael Schweitzer and Bertrand did some work a few years
                    back that included variations of COMPARABLE such as partial ordering.
                    Does it make any sense for me to dig that out, or is it enough
                    to just work on COMPARABLE for the time being?

                    Hope this helps,
                    -- Jim

                    >
                    > 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
                    >
                    >
                    > ---------------------------
                    >
                    > http://www.eiffel-nice.org/
                    >
                    > --------------------------
                    >
                    > Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/
                    >
                    >
                    >
                  • Arno Wagner
                    ... Thanks for the confidence! I ll do my best. I am sure it will be a learning experience though. As for your comments, I might post a detailed answer in the
                    Message 9 of 9 , Aug 9, 2002
                    • 0 Attachment
                      On Fri, Aug 09, 2002 at 12:01:39PM -0400, James McKim wrote:
                      > Hey Arno,
                      >
                      > Thanks for taking the lead, both for the group in
                      > general and for COMPARABLE in particular. I'm sure
                      > you'll do a great job!

                      Thanks for the confidence! I'll do my best.
                      I am sure it will be a learning experience though.

                      As for your comments, I might post a detailed answer
                      in the next days, but I have a wacky idea now:

                      [...]
                      > I like this change, but note that actually we can do it
                      > entirely in terms of `<' as the basic specifier for
                      > COMPARABLE.
                      [...]

                      We can, but it has some interesting consequences. If
                      we do a total order in terms of `<' only, that means
                      that equality will be defined in terms of `<' only.
                      (Equality is needed because of totality unless we
                      allow only `='-equality.)
                      Let `===' denote this type of "equality with respect
                      to `<'" for the moment.

                      The definition for `===' would be

                      for all a,b:
                      a === b if and only if ( not(a<b) and not(b<a) )

                      neatly enforcing totality of `<'. (Although probably
                      not quite in the way people expect. `===' would
                      be kind of a kernel relation here.) Without `==='
                      the problem would be that not(a<b) and not(b<a)
                      could be true, while a and b are not the same
                      object. This would make `<' partial.

                      If we spin this a little further, we can indeed use
                      the above definition of "equality with respect to `<'"
                      and define all the other operators according to it.

                      `>',`<=',`>=' are no problem. `===' is not even needed here.

                      max(a,b):
                      if a>b then max(a,b) = a
                      if b>a then max(a,b) = b
                      if a===b then max(a,b) = a or max(a,b) = b

                      `min' analog.

                      `three_way_comparison' analog.


                      Added benefit: `is_equal' does not make an appearence
                      in this at all! `===' and `is_equal' are completely
                      independent. Getting rid of the forced relation between
                      `===' and `is_equal' _would_ be nice in mu opinion.
                      (Everybody that wants this relation can still define
                      `<' accordingly.)


                      The one problem I see is what to do with `==='?

                      - First option: Redefine `is_equal' to
                      have the semantics of `==='. That is how it was done
                      up to now. Problem: `is_equal' is sort of a 'higher'
                      concept than `<'. To me it feels wrong to change the
                      basic notion of equality in order to accomodate the
                      less basic notion of order.

                      - Second option: Have a new explicit operator `==='
                      (naming to be determined). Would this operator really
                      offer an added benefit or just clutter the interface?
                      Personally I might prefer this one.

                      - Third option: Do not have an explicit `===' operator.
                      It is not a good idea to have a defined notion
                      for equality (`===') but no explicit name/operator for it,
                      so this is probably not be the way to go.

                      - Fourth option: Have `===' defined as `is_equal'
                      and constrain `<' accordingly. This would make sense
                      insofar as `is_equal' is meta-equality in Eiffel. On the
                      other hand we might just want a special kind of equality
                      with regard to order and constraining `<' is indeed not
                      elegant. (This was my original proposal.)

                      - Fifth option: Define `===' as `='. This seems very
                      constraining. On the other hand, is this not what we are
                      thinking of when we say "ordered"? Mathematically it is.

                      This option has one strong benefit: It ensures
                      that objects can always be sorted/orderd in one way only.
                      Of two different opjects one will always be larger.
                      In a sense all the other options above are only there
                      because we allow an equivalence relation (`is_equal') to
                      take the place of equality, but at the same time cannot do
                      a complete factoring, i.e. things that are equal via
                      `is_equal' can still be distinguished.

                      - Other ideas ??

                      This totality requirement has indeed some interesting
                      consequences....

                      Regards,
                      Arno

                      P.S.: I don't think a discussion about partial orders will
                      help us much. There are many types of these and often you
                      actually want a lattice, making things even more general
                      and the number of variants very, very large. So unless you
                      have this papers handy, don't bother.

                      ---
                      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
                    Your message has been successfully submitted and would be delivered to recipients shortly.