How do I use an across loop in post condition to compare an old array and new array at certain indices?

Question

I have a method that shifts all the items, in an array, to the left by one position. In my post condition I need to ensure that my items have shifted to the left by one. I have already compared the first element of the old array to the last element of the new array. How do i across loop through the old array from 2 until count, loop through the new array from 1 until count-1 and compare them? This is my implementation so far.

        items_shifted:
                    old array.deep_twin[1] ~ array[array.count]
                        and
                    across 2 |..| (old array.deep_twin.count) as i_twin all
                        across 1 |..| (array.count-1) as i_orig  all
                            i_twin.item ~ i_orig.item
                            end
                        end



    end

I expected the result to be true but instead I get a contract violation pointing to this post condition. I have tested the method out manually by printing out the array before and after the method and I get the expected result.

Answer 1

In the postcondition that fails, the loop cursors i_twin and i_orig iterate over sequences 2 .. array.count and 1 .. array.count - 1 respectively, i.e. their items are indexes 2, 3, ... and 1, 2, .... So, the loop performs comparisons 2 ~ 1, 3 ~ 2, etc. (at run-time, it stops on the first inequality). However, you would like to compare elements, not indexes.

One possible solution is shown below:

    items_shifted:
        across array as c all
            c.item =
                if c.target_index < array.upper then
                    (old array.twin) [c.target_index + 1]
                else
                    old array [array.lower]
                end
        end

The loop checks that all elements are shifted. If the cursor points to the last element, it compares it against the old first element. Otherwise, it tests whether the current element is equal to the old element at the next index.

Cosmetics:

1. The postcondition does not assume that the array starts at 1, and uses array.lower and array.upper instead.

2. The postcondition does not perform a deep twin of the original array. This allows for comparing elements using = rather than ~.

Edit: To avoid potential confusion caused by precedence rules, and to highlight that comparison is performed for all items between old and new array, a better variant suggested by Eric Bezault looks like:

    items_shifted:
        across array as c all
            c.item =(old array.twin)
                [if c.target_index < array.upper then
                    c.target_index + 1
                else
                    array.lower
                end]
        end