向方法添加修改会破坏循环不变量答案

【问题标题】：Adding modifies to a method breaks loop invariant向方法添加修改会破坏循环不变量
【发布时间】：2021-04-23 01:38:59
【问题描述】：

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

我已经通过将该循环提取到它自己的方法中来解决这个问题，但是感觉很hacky。

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，但是我找不到如何做到这一点？

【问题讨论】：

标签： dafny

【解决方案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 会为您推断。

【讨论】：