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

STRING 'out'

Expand Messages
  • Roger Browne
    ... I only looked at changes that were needed to make the postconditions usable in a descendant. I didn t look into simplifications that became possible due to
    Message 1 of 4 , Jun 13, 2001
    • 0 Attachment
      James McKim wrote:
      > Yes, there will likely be a number of these, though I know
      > Roger made a first pass.

      I only looked at changes that were needed to make the postconditions
      usable in a descendant. I didn't look into simplifications that became
      possible due to the addition of features 'string' and 'same_string'.

      > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      > > out: STRING
      > > -- New string containing terse printable representation
      > > -- of current object.
      > > ensure
      > > out_not_void: Result /= Void
      > > same_items: Result.same_type (Current)
      > > implies Result.is_equal (Current)
      > > new_string: Result /= Current
      > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      >
      > Also, for this one, I can't remember
      > why we included 'new_string' since I think we agreed that
      > a comment of the form that's included here was enough to
      > guarantee that a new string object must be created
      > each time.

      We discussed this (in the context of several other features), and in each
      of those other cases we decided to use the comment "new string" instead
      of trying to partially-capture that constraint with an assertion.

      However, for 'out' we specifically decided not to follow our usual
      policy, because we wanted to make it very clear that the simple-minded
      implementation ("result := current") was not correct.

      Eric wrote:
      > > Now that we have `same_string', we can perhaps rewrite
      > > the postcondition "same_items" as follows:
      > >
      > > same_items: Result.same_string (Current)

      That would work for class STRING, but doesn't capture the semantics that
      we intended. The motivating example was a descendant of STRING that adds
      another attribute (for example, a 'language' field). In that descendant,
      it would be reasonable to allow the following as results of 'out':

      plate of fish (English)
      sur le pont (French)
      ostconditionpay (Pig Latin)

      We added the 'same_type' condition so that the specification only
      constrained the behaviour of 'out' in class STRING.

      I'm not suggesting that these things cannot be changed. I'm just pointing
      out that they were not oversights; there were clear reasons for making
      those decisions at the time.

      Regards,
      Roger
      --
      Roger Browne - roger@... - Everything Eiffel
      19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
    • Eric Bezault
      ... OK, sorry I forgot about that. ... Not quite. This postcondition also constrains descendant classes: class COLORED_STRING inherit STRING redefine out end
      Message 2 of 4 , Jun 13, 2001
      • 0 Attachment
        Roger Browne wrote:
        >
        > That would work for class STRING, but doesn't capture the semantics that
        > we intended. The motivating example was a descendant of STRING that adds
        > another attribute (for example, a 'language' field). In that descendant,
        > it would be reasonable to allow the following as results of 'out':
        >
        > plate of fish (English)
        > sur le pont (French)
        > ostconditionpay (Pig Latin)

        OK, sorry I forgot about that.

        > We added the 'same_type' condition so that the specification only
        > constrained the behaviour of 'out' in class STRING.

        Not quite. This postcondition also constrains descendant
        classes:

        class COLORED_STRING

        inherit

        STRING
        redefine
        out
        end

        feature

        out: STRING is
        -- New string containing terse printable representation
        -- of current object.
        do
        Result := clone (Current)
        end


        >
        > I'm not suggesting that these things cannot be changed. I'm just pointing
        > out that they were not oversights; there were clear reasons for making
        > those decisions at the time.
        >
        > Regards,
        > Roger
        > --
        > Roger Browne - roger@... - Everything Eiffel
        > 19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
        >
        > ---------------------------
        >
        > http://www.eiffel-nice.org/
        >
        > --------------------------
        >
        > Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/

        --
        Eric Bezault
        mailto:ericb@...
        http://www.gobosoft.com
      • Eric Bezault
        Sorry, I pressed on Send by accident in my previous message. ... OK, sorry I forgot about that. ... Not quite. This postcondition also constrains descendant
        Message 3 of 4 , Jun 13, 2001
        • 0 Attachment
          Sorry, I pressed on "Send" by accident in my previous message.

          Roger Browne wrote:
          >
          > That would work for class STRING, but doesn't capture the semantics that
          > we intended. The motivating example was a descendant of STRING that adds
          > another attribute (for example, a 'language' field). In that descendant,
          > it would be reasonable to allow the following as results of 'out':
          >
          > plate of fish (English)
          > sur le pont (French)
          > ostconditionpay (Pig Latin)

          OK, sorry I forgot about that.

          > We added the 'same_type' condition so that the specification only
          > constrained the behaviour of 'out' in class STRING.

          Not quite. This postcondition also constrains descendant
          classes:

          class COLORED_STRING

          inherit

          STRING
          redefine
          out
          end

          feature

          out: STRING is
          -- New string containing terse printable representation
          -- of current object.
          do
          Result := clone (Current)
          end

          The following comment should say more clearly that a "new STRING"
          has to be exactly of type STRING. Is a COLORED_STRING objects
          a "new-created STRING"? I guess the answer is no, but it should
          be stated unambiguously.

          -- 4. The phrase "new STRING" in a header comment means a
          -- newly-created STRING to which there is no reference other than
          -- from 'result'.

          --
          Eric Bezault
          mailto:ericb@...
          http://www.gobosoft.com
        Your message has been successfully submitted and would be delivered to recipients shortly.