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

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

Expand Messages
  • Alexander Kogtenkov
    ... What about old lower = 13 old upper = 16 min_index = 5 max_index = 4 ? As old subarray is evaluated anyway - this is the real life: all Eiffel compilers
    Message 1 of 31 , Nov 12, 2001
    • 0 Attachment
      Roger Browne wrote:

      > The guard expression at the beginning of 'stable_in_intersection'
      > aims to
      > ensure that we only check the rest of 'stable_in_intersection' if
      > there
      > is in fact an intersection. The intersection could still be an empty
      > array, e.g. with:
      >
      > old lower = 3
      > old upper = 6
      > min_index = 5
      > max_index = 4
      >
      > But the guard at the beginning of 'stable_in_intersection', combined
      > with
      > the precondition, should ensure that we do not attempt to evaluate
      > 'subarray' with invalid arguments.

      What about

      old lower = 13
      old upper = 16
      min_index = 5
      max_index = 4

      ?

      As "old subarray" is evaluated anyway - this is the real life: all
      Eiffel compilers do it - the precondition to this "old subarray" is
      broken.

      Regards,
      Alexander Kogtenkov
      Object Tools, Moscow
    • 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.