如何在前提条件下迭代数组？

Question

我想在前提条件下循环访问数组。但似乎前提条件部分不允许使用 "from" 和 "across" 语法。

有没有办法在前提条件下遍历数组？

insert_last (s: STRING)
require
    new_is_longer_than_prevs:
-- here I want to iterate through array "arr" and if length of s is longer than all other previously stored string values in array
do
    arr.force (s, arr.upper + 1)
end

Answer 1

您可以在前置条件和后置条件中使用 'across ... as ... all ... end' 或 'across ... as ... some ... end'。 'all' 版本用于在每次迭代的条件为真时有效，而 'some' 版本用于在至少一次迭代的条件为真时有效。您可以在代码中使用类似这样的东西：

insert_last (s: STRING)
    require
        new_is_longer_than_prevs: 
            across arr.lower |..| arr.upper as la_index all s.count > arr[la_index.item].count end
    do
        arr.force (s, arr.upper + 1)
    end

Answer 2

其他回复中建议的版本在大多数情况下都有效（它假定数组的较低索引为 1）。但是，可以直接在数组上而不是在它的索引范围上使用跨循环：

new_is_longer_than_prevs:
    across arr as c all s.count > c.item.count end

此版本适用于任何较低的索引，并且在运行时效率稍高。

如何在前提条件下迭代数组？

How to iterate array in precondition?

eiffel