对方法进行修改会破坏循环不变式

Question

最重要的问题是，当我向一个方法添加修改时，突然我的一些循环不变量不再正确检查。

我通过将循环提取到它自己的方法中来解决这个问题，但是这感觉非常粗糙。

method Merge (arr : array<int>, l : int, m : int, r : int) returns (res : array<int>)
requires 0 <= l < m < r <= arr.Length
requires sorted_slice(arr, l, m);
requires sorted_slice(arr, m, r);
ensures sorted_slice(res, l, r)
{
var ia := l;
var ib := m;
res := new int[r - l];
var ri := 0;
while ri < res.Length
decreases res.Length - ri
invariant ri == (ia - l) + (ib - m)

//Ensure that the ia/ib is within the sorted slice at all times
invariant l <= ia <= m
invariant m <= ib <= r
// r[:ri] is sorted
invariant forall j, k :: (0 <= j <= k < ri) && (0 <= j <= k < res.Length) ==> res[j] <= res[k]
invariant forall ja, jr :: (ia <= ja < m) && (0 <= jr < ri < res.Length) ==> res[jr] <= arr[ja]
invariant forall jb, jr :: (ib <= jb < r) && (0 <= jr < ri < res.Length) ==> res[jr] <= arr[jb]
{
if ia >= m {
res[ri] := arr[ib];
ib := ib + 1;
ri := ri + 1;
} else if ib >= r {
res[ri] := arr[ia];
ia := ia + 1;
ri := ri + 1;
} else {
if arr[ia] < arr[ib]
{
res[ri] := arr[ia];
ia := ia + 1;
ri := ri + 1;
} else {
res[ri] := arr[ib];
ib := ib + 1;
ri := ri + 1;
}
}
}
...
}

特别是当我将modifies arr添加到Merge的签名中时，第4和第5个循环不变量失败。

为什么会发生这种情况?我可以理解，我可能需要在循环中添加一个不变量，说它不编辑arr，但我找不到如何做到这一点?

Answer 1

循环继承封闭方法[0]的任何modifies子句。所以，如果你的方法说的是modifies arr，那么，实际上，你的循环也是。这意味着验证者将把循环视为可能修改arr的元素，无论循环体是否真的这样做[1]。因此，您确实需要在循环规范中添加一些内容，说明循环实际上不会修改arr。

你的方法也可以修改res的元素，因为数组res是"新分配的"。在方法内部。这意味着你的循环可以同时修改arr和res，如果你的方法是modifies arr。

因此，您想要重写继承的modifies子句，以便您可以将循环的有效modifies子句限制为仅res。为此，写入

modifies res

在循环的decreases和invariant子句中。

细分，仅供参考:

• [0]对于嵌套循环，内部循环继承外围循环的有效modifies子句。
• [1]如果验证者可以通过简单的语法扫描确定循环体不可能修改堆中的任何内容，那么验证者将使用这一事实，而不考虑modifies子句。
• 顺便说一句，对于你的程序，你可以省略显式的decreases子句，因为Dafny会为你推断出来。