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

COMPARABLE and equality.

Expand Messages
  • Arno Wagner
    Hi, I agree with Jim that
    Message 1 of 4 , Aug 16, 2002
      Hi,

      I agree with Jim that '<' should be the one and only basic
      specifier. The central question is how to specify equality.
      When I tried to assess the degree or freedom we have, I
      ran into a surprising thing.

      The fundamental choice is: Should 'is_equal' be the
      equality operator for COMPARABLE or should there be
      a special equality operator. In order to see what
      freedom we have, I made an attempt to define this freedom
      exactly. I made two surprising discoveries:

      1. There is not much freedom at all.
      2. Implicit type constraints on arguments resulting from
      contracts.

      I had not been aware of the second one. The basic example is

      frozen standard_is_equal (other: like Current): BOOLEAN

      which has a postcondition

      symmetric: Result implies other.standard_is_equal (Current)

      In order for the call to 'standard_is_equal' in the postcondition
      to be denifed, 'Current' needs to be 'like other'.

      VNCH (4th item) implies that 'symmetric' is correctly typed
      only if 'Current' and 'other' have the same actual type
      at run-time. This looks very much like an implicit type
      constraint to me! (The reasoning is that for correct typing
      in 'symmetric', 'Current' has to conform to 'like other'
      and by VNCH to 'other' itself at run-time. At the same time
      'other' has to conform to 'current' at run time. )

      To validate this I did some experimentation with SE that
      did not enlighten me: Given a class TA and a child TB of TA,
      with 'a' an instance of TA and 'b' an instance of TB, I could
      compile and call

      a.standard_is_equal(b)

      where the postcondition to be evaluated after partial
      value substitution is

      symmetric: Result implies b.standard_is_equal(a)

      which should give a run-time type error but does not.

      When I add a 'test_is_equal' to TA (with a result that
      does not matter, but the same signature and similar
      contract as standard_is_equal), and then call

      a.test_is_equal(b)

      I actually get a run-time type error from the postcondition
      as VNCH seems to imply I should get. (The classes are attached
      at the end.)

      wagner ~/exp/eiffel/types_contracts>./a.out
      Line : 20 column 36 in ./a.e.
      *** Error at Run Time *** :
      Target is not valid (not the good type).
      Expected: "B", Actual: "A".
      6 frames in current stack.
      ===== Bottom of run-time stack =====
      ...

      That means that at least in SE the postcondition
      'symmetric' of 'standard_is_equal' is implemented as
      a special case. And it seems to be wrong!


      Have I gotten this right? Is this actually
      an implicit way to check run-time type equality for
      two arguments to an operator?



      The reason I stumbled over this is that any type of
      equality in COMPARABLE must at least have this contract:

      infix "===" (other: like Current): BOOLEAN is
      require
      other_exists: other /= Void
      ensure
      totality: Result =
      (not (Current < other) and not (other < Current))

      (Name proposal for the added postcondition would be 'totality'
      instead of 'trichotomy'.) There is really no choice in this,
      as this is the only postcondition that ensures totality of the
      order relation.


      Now the postcondition can only be evaluated if 'other'
      and 'Current' have the same type (bacause '<' specifies
      the second argument as 'like Current'). Furthermore
      the rest of the contract of 'is_equal' from GENERAL is
      now implicitely present:

      - 'symmetric' because of 'totality'.
      - 'same_type' does not apply, a call with different types
      is not possible anyway.
      - 'consistent' is no problem as (other suprise)
      'standard_is_equal' is the same as '=' for all
      types except ARRAY and STRING (says ETL in section 19.7
      when taking the field 'object_id' from GENERAL into account).

      All in all that means we have something very close to an 'is_equal'
      with added postcondition 'totality'. If that is true, we can just
      clean up the present COMPARABLE a bit, as we cannot get away
      from something very similar to the current form anyway. I feel
      that a new operator that has the sole purpose of avoiding
      the strengthening of the postcondition of 'is_equal', but
      does in effect offer that funcionality, is redundant.

      It all depends on whether my understanding of the typing
      rules is correct. If it is, we should also think about adding
      constraints to contracts that make this obvious, e.g. in the form

      symmetric: Result implies other.standard_is_equal (Current)
      same_types: same_type(other) -- implication of 'symmetric'


      Furthermore postconditions like

      same_type: Result implies same_type (other)

      on 'standard_is_equal' in GENERAL can be removed. They do not apply
      at all and are misleading. By my reasoning above 'same_type(other)'
      is already part of the contract. However there is the small problem
      that at least SE does it wrong and other compilers may also, since
      ETL implies that different types can be compared with
      'standard_is_equal' and associated features (section 19.7 in ETL).
      Of course ETL does not have 'symmetric' in the postcondition
      of 'standard_is_equal'. This is possibly not an oversight.

      Any insights?

      Regards,
      Arno




      The exapmle that should produce a run-time type error,
      but does not (SE -0.74):
      -----------------------------------
      class A
      creation make_a
      feature
      one: INTEGER

      make_a(value: INTEGER) is
      do
      one := value
      end
      end
      ------------------------------------
      class B
      inherit A
      creation make_b
      feature
      make_b(value: INTEGER; value2: INTEGER) is
      do
      one := value
      two := value2
      end

      two: INTEGER
      end
      -------------------------------------
      class COMPARE
      creation make
      feature
      make is
      local
      a: A
      b: B
      do
      create a.make_a(1)
      create b.make_b(2,3)
      print(a.standard_is_equal(b).to_string+"%N")
      end
      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


      --
      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
    • Arno Wagner
      P.S.: There are two questions here: 1. Do we get a same_type implicit assertion on the equality in COMPARABLE as a consequence of totality? Seems to me like
      Message 2 of 4 , Aug 16, 2002
        P.S.: There are two questions here:

        1. Do we get a 'same_type' implicit assertion on
        the equality in COMPARABLE as a consequence
        of totality?

        Seems to me like that, unless I did overlook something.

        2. What about the postcondition 'symmetric' on
        'standard_is_equal' (and associates) in GENERAL?
        Does it need revision? Or does it need bug-fixes
        in the compiler(s)?

        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
      • Emmanuel STAPF [ES]
        Hi, I should have asked the question when the discussion about COMPARABLE started, but could someone summarize what is wrong with the existing specification of
        Message 3 of 4 , Aug 16, 2002
          Hi,

          I should have asked the question when the discussion about COMPARABLE
          started, but could someone summarize what is wrong with the existing
          specification of the class in ELKS 95. My believe is that we should try
          to fix bugs if any, to ensure that assertions are well defined (like we
          did in ARRAY and STRING) and then try to find solutions for mismatch
          between different Eiffel vendors.

          Manu

          ----------------------------------------------------------
          Eiffel Software
          805-685-1006
          http://www.eiffel.com
          Customer support: http://support.eiffel.com
          Product information: info@...
          ----------------------------------------------------------
        • Arno Wagner
          ... Right. From my point of view there is only one major issue in COMPARABLE: Is it right to use is_equal for equality. At the moment it looks to me like
          Message 4 of 4 , Aug 16, 2002
            On Fri, Aug 16, 2002 at 04:06:07PM -0700, Emmanuel STAPF [ES] wrote:
            > Hi,
            >
            > I should have asked the question when the discussion about COMPARABLE
            > started, but could someone summarize what is wrong with the existing
            > specification of the class in ELKS 95. My believe is that we should try
            > to fix bugs if any, to ensure that assertions are well defined (like we
            > did in ARRAY and STRING) and then try to find solutions for mismatch
            > between different Eiffel vendors.
            >
            > Manu

            Right. From my point of view there is only one major issue
            in COMPARABLE: Is it right to use 'is_equal' for equality.
            At the moment it looks to me like there is not much choice
            anyway.

            In the process of thinking about this, I stumbled over the
            possible problem with the "equality" features in GENERAL,
            which I mainly posted to be sure I understood it, and if
            I do, to mark as something to be done when next visiting
            GENERAL.

            There are some minor things in the specifiation (invariants,
            preference of min/max of the first argument, postconditions),
            that do however not have any or any major impact on
            functionality. I do not see any code being broken by any
            of the discussed changes, as they all just relax the
            specification or re-formulate it.

            See Jim's and my last post for the equality question.
            See my initial post or Jim's last post for the minor things.

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