Re: [eiffel-nice-library] Inconsistency between ARRAY resize postcondition and subarray precondition
- James McKim wrote:
>This is fine, but isn't the point of resize that for each item in both
> 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.
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
>What I meant was that there were no pathological cases in which non-zero
> > 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....
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
> > 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.
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
- James McKim wrote:
> Roger,Thanks Jim, you are right. It's the 7 NOVEMBER version which had the "a
> If you look at these closely I think you'll find that they
> are equivalent and both written by you. I concur with both :-).
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'.
valid_bounds: min_index <= max_index + 1
new_lower: lower = min_index
new_upper: upper = max_index
min_index < old lower implies subarray
(min_index, max_index.min (old lower - 1)).all_default
max_index > old upper implies subarray
(min_index.max (old upper + 1), max_index).all_default
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!
Roger Browne - roger@... - Everything Eiffel
19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428