如何在 post 条件下使用交叉循环来比较某些索引处的旧数组和新数组？

Question

我有一种方法可以将数组中的所有项目向左移动一个位置。在我的 post 条件下，我需要确保我的项目已向左移动一位。我已经将旧数组的第一个元素与新数组的最后一个元素进行了比较。我如何从 2 到 count 遍历旧数组，从 1 到 count-1 遍历新数组并比较它们？到目前为止，这是我的实施。

        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

我原以为结果是真的，但我却收到了指向此 post 条件的合同违规。我通过打印方法前后的数组手动测试了方法，得到了预期的结果。

Answer 1

在失败的后置条件中，循环游标i_twin和i_orig分别迭代序列2 .. array.count和1 .. array.count - 1，即它们的项是索引2, 3, ... 和 1, 2, ...。因此，循环执行比较 2 ~ 1、3 ~ 2 等（在运行时，它在第一个不等式处停止）。但是，您想比较元素，而不是索引。

一种可能的解决方案如下所示：

    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

循环检查是否所有元素都已移位。如果光标指向最后一个元素，它会将它与旧的第一个元素进行比较。否则，它测试当前元素是否等于下一个索引处的旧元素。

化妆品：

后置条件不假设数组从1开始，而是使用array.lower和array.upper代替。
后置条件不执行原始数组的深度孪生。这允许使用 = 而不是 ~.

编辑： 为了避免由优先规则引起的潜在混淆，并强调对旧数组和新数组之间的所有项目进行比较，Eric Bezault 建议的更好的变体看起来喜欢：

    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

如何在 post 条件下使用交叉循环来比较某些索引处的旧数组和新数组？

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

eiffel

post-conditions