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

Re: [eiffel-nice-library] Inconsistency between ARRAY resize postcondition and subarray precondition

Expand Messages
  • Roger Browne
    OK, I think we can now wrap up the discussion of resize . ... Yes, that was one factor. At the time, the SmallEiffel version of is_equal also had
    Message 1 of 31 , Nov 6, 2001
    • 0 Attachment
      OK, I think we can now wrap up the discussion of 'resize'.

      Peter Horan asked:
      > ... why was is_equal not used [in the postcondition
      > of 'resize'] which would insist that each item was
      > accessed by a stable index?
      > ...
      > BTW, is_equal in ISE V4.5 = same_items in
      > ELKS 2000 - maybe that had something to do with it?

      Yes, that was one factor. At the time, the SmallEiffel version of
      'is_equal' also had non-standard behaviour. Another reason was that, at
      the time we specified 'resize', we hadn't yet specified 'is_equal' in
      detail.

      Although the postcondition of 'resize' could be formulated in terms of
      'is_equal', I'm quite happy to keep the existing style which is phrased
      in terms of 'same_items' and explicit tests on 'lower' and 'upper'.

      Anyway, here's a candidate version for a corrected specification of
      'resize'.

      6 NOVEMBER 2001 VERSION:

      resize (min_index, max_index: INTEGER)
      -- Resize to bounds `min_index' and `max_index'.
      -- Do not lose any item whose index is in both
      -- `lower..upper' and `min_index..max_index'.
      require
      valid_bounds: min_index <= max_index + 1
      ensure
      new_lower: lower = min_index
      new_upper: upper = max_index
      default_if_too_small:
      min_index < old lower implies subarray
      (min_index, max_index.min (old lower - 1)).all_default
      default_if_too_large:
      max_index > old upper implies subarray
      (min_index.max (old upper + 1), max_index).all_default
      stable_in_intersection:
      subarray ((min_index.max (old lower)).min(max_index + 1),
      (max_index.min (old upper)).max(min_index - 1)).same_items
      (old subarray ((min_index.max (lower)).min(upper + 1),
      (max_index.min (upper)).max(lower - 1)))

      This candidate version is equal to the ELKS 2000 version except that the
      'stable_in_intersection' clause has been replaced by the one posted by
      James McKim on 24 October.

      Here's the old (ELKS 2000) version of that clause:

      stable_in_intersection:
      subarray ((min_index.max (old lower)).min(old upper + 1),
      (max_index.min (old upper)).max(old lower - 1)).same_items
      (old subarray ((min_index.max (lower)).min(upper + 1),
      (max_index.min (upper)).max(lower - 1)))

      If no problems show up with the 6 NOVEMBER 2001 version, I'll put it to a
      vote in a couple of days.

      Regards,
      Roger
      --
      Roger Browne - roger@... - Everything Eiffel
      19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
    • Roger Browne
      ... Thanks Jim, you are right. It s the 7 NOVEMBER version which had the a implies old b gotcha. The 12 NOVEMBER and 13 NOVEMBER versions are equivalent and
      Message 31 of 31 , Nov 14, 2001
      • 0 Attachment
        James McKim wrote:

        > Roger,
        >
        > If you look at these closely I think you'll find that they
        > are equivalent and both written by you. I concur with both :-).

        Thanks Jim, you are right. It's the 7 NOVEMBER version which had the "a
        implies old b" gotcha. The 12 NOVEMBER and 13 NOVEMBER versions are
        equivalent and free of this gotcha.

        Recent comments still show a preference for the "or else" version (with
        Arno's preference for the "implies" version noted). I'll start a vote
        tomorrow on the "or else" version unless something new crops up. Here it
        is again (unchanged):

        13 NOVEMBER 2001 VERSION:

        resize (min_index, max_index: INTEGER)
        -- Resize to bounds `min_index' and `max_index'.
        -- Do not lose any item whose index is in both
        -- `lower..upper' and `min_index..max_index'.
        require
        valid_bounds: min_index <= max_index + 1
        ensure
        new_lower: lower = min_index
        new_upper: upper = max_index
        default_if_too_small:
        min_index < old lower implies subarray
        (min_index, max_index.min (old lower - 1)).all_default
        default_if_too_large:
        max_index > old upper implies subarray
        (min_index.max (old upper + 1), max_index).all_default
        stable_in_intersection:
        max_index < old lower or min_index > old upper or else
        subarray (min_index.max (old lower).min (max_index + 1),
        max_index.min (old upper).max(min_index - 1)).is_equal
        (old subarray (min_index.max (lower).min(upper + 1),
        max_index.min (upper).max(lower - 1)))

        Thanks for everyone's patience. This stuff can get hard!

        Regards,
        Roger
        --
        Roger Browne - roger@... - Everything Eiffel
        19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
      Your message has been successfully submitted and would be delivered to recipients shortly.