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

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

Expand Messages
  • Peter Horan
    ... This is fine, but isn t the point of resize that for each item in both the original and resized array, the index is unaltered? same_items is blind to this.
    Message 1 of 31 , Oct 28, 2001
    • 0 Attachment
      James McKim wrote:
      >
      > Peter Horan wrote:
      > >
      > > James McKim wrote:
      > >
      > > > This is OK, I think. We're using same_items not is_equal so
      > > > the bounds don't have to match. In fact, it's kind of neat.
      > > > It couldn't find an intersection, so it picked the two legal
      > > > subarrays that were _closest_ to intersecting.
      > >
      > > I thought about this a little more, also.
      > >
      > > I began to worry about using same_items, because it returns True when
      > > the items are the same but the domain [lower...upper] of the two arrays
      > > differ.
      >
      > But this is just what we wanted. Among many other advantages it
      > provides an easy way to compare my array to a subarray of yours.

      This is fine, but isn't the point of resize that for each item in both
      the original and resized array, the index is unaltered? same_items is
      blind to this. But, I see that my concern is covered by new_lower: lower
      = min_index and new_upper: upper = max_index
      >
      > >
      > > I have not investigated if there is a case in which two non-zero
      > > intervals can be generated. In the absence of proving it myself, I think
      > > it is OK if they overlap, because this would have shown up at the time
      > > of constructing the postcondition.
      >
      > Lost you here. Certainly during a resize the new array could overlap the
      > old one....

      What I meant was that there were no pathological cases in which non-zero
      sized, non-overlapping arrays could be compared with same_items. But
      when I realised that expressions such as "min_index.max (old
      lower)).min(old upper + 1)" can only have three values, namely, in
      non-decreasing order, old lower (when min_index < old lower), min_index
      or old upper + 1 (min_index >= old upper), it is evident that
      non-overlapping cases will generate zero-sized arrays in this
      comparison.
      >
      > >
      > > But, why was is_equal not used which would insist that each item was
      > > accessed by a stable index?
      >
      > One reason is above. I think the other was that is_equal inherits some
      > assertions that we didn't want to be burdened with.

      Ah.

      Too summarise, I am now happy with the use of same_items, and I am happy
      that if an array is resized to an interval outside its domain, the
      postcondition reports correctly.
      --
      Peter Horan School of Computing and Mathematics
      peter@... Deakin University
      +61-3-5227 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA
      +61-3-5227 2028 (FAX) http://www.cm.deakin.edu.au/~peter

      -- The Eiffel guarantee: From specification to implementation
      -- (http://www.cetus-links.org/oo_eiffel.html)
    • 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.