Same arrays indexed differently are not equal

[Marco Piccioni]

Hi,

The following code:

f
local
array1: ARRAY[STRING]
array2: ARRAY[STRING]
s: STRING
do
create s.make_from_string(“foo”)
create array1.make_filled (s,0,0)
create array2.make_filled (s,1,1)
print ((array1 ~ array2).out) -----False
end

invoking compare_objects on both arrays doesn’t work either.

Is it really so or am I missing something?

My point is that if two arrays contain the same object they should be considered “equal” irrespectively of how the elements are indexed internally.

Thanks!
Marco

[Alexander Kogtenkov]

Array comparison does take boundaries into account. I guess, one would expect the following to be correct code:

 

if a ~ b and then a.valid_index (i) then

    check

         b.valid_index (i)

    end

end

 

BTW, arrays are instances of TABLE, and I would expect rows to be located at the same keys for equal tables (`valid_index` is `valid_key` in TABLE).

 

Probably, what you are looking for is `same_items`. It compares items regardless of indexing. However, it always uses equality for comparison, and ignores `object_comparison`.

 

Alexander Kogtenkov

 

 

Marco Piccioni <mallo.p...@gmail.com>:

[jjj]

Regarding indexing...

Does calling `rebase (0)' on an ARRAY just index the same items starting from zero, or does the array lose the last item from the old array and put a default value at index zero?  Is `count' the same?

jjj

 

[Alexander Kogtenkov]

The postcondition of `rebase` is

 

            lower_set: lower = a_lower
            upper_set: upper = a_lower + old count - 1

 

The postcondition of `count` is

 

            consistent_with_bounds: Result = upper - lower + 1

 

With that, `upper_set` can be rewritten as

 

            upper_set: upper = old upper + (a_lower - old lower)

 

Therefore, `rebase` simply shifts the indexes by positioning the first element at the specified lower index without changing the number of elements in the array. This answers the question about `count`: it remains the same.

 

Unfortunately, the postcondition does not say much about elements themselves. Fortunately, the feature does preserve them. The following predicate

 

            same_items (old (create {ARRAY [G]}.make_from_array (Current)))

 

might be a potential additional postcondition subclause.

 

Alexander Kogtenkov

 

 

jjj <jjj...@uky.edu>:
 

Regarding indexing...

 

Does calling `rebase (0)' on an ARRAY just index the same items starting from zero, or does the array lose the last item from the old array and put a default value at index zero?  Is `count' the same?

 

jjj

 

 

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/eiffel-users/e279c71e-e3e8-4f8c-8709-d783eec1c028o%40googlegroups.com.