向方法添加修改会破坏循环不变性

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 在方法内部是“新分配的”。这意味着如果您的方法说 modifies arr.

，则允许您的循环修改 arr 和 res

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

modifies res

在循环的 decreases 和 invariant 子句中。

精分，仅供参考：

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

向方法添加修改会破坏循环不变性

Adding modifies to a method breaks loop invariant

dafny