如何在前提条件中迭代阵列

Question

我想在先决条件下通过数组迭代。但似乎前提部分不允许使用"来自"one_answers"跨"语法。

有没有办法在前提条件中迭代阵列？

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

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

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

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

Answer 2

您可以使用'跨... as ... ass ... end'或'and ... as ...某些...在前提条件和后条件中结束'。如果每次迭代都是正确的，则"所有"版本用于有效，并且"某些"版本至少在一个迭代中为true，则使用"某些"版本有效。您可以在代码中使用类似的东西：

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