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

问题描述

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

我通过将该循环提取到它自己的方法中来解决这个问题，但是这感觉很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,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，但是我找不到如何做到这一点？

解决方法

循环继承封闭方法 [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 会为您推断出来。