在Dafny中证明归并排序：Merge方法后置条件验证出错

问题核心：现有代码的while循环缺少关键不变量，Dafny没法自动推导出循环过程中merged始终有序，也无法确认merged末尾元素和剩余待合并元素的大小关系，导致最终的sorted(merged)后置条件验证失败。

要补充的关键修改 #

给while循环加上3个核心不变量，再在合并剩余元素前添加辅助断言，就能让验证通过：

修改后的完整代码 #

predicate sorted(s: seq<int>)
{
  forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

method Merge(left: seq<int>, right: seq<int>) returns (merged: seq<int>)
    requires sorted(left) && sorted(right)
    ensures sorted(merged)
    ensures |merged| == |left| + |right|
{
    var i := 0;
    var j := 0;
    merged := [];

    while i < |left| && j < |right|
        invariant 0 <= i <= |left|
        invariant 0 <= j <= |right|
        invariant |merged| == i + j
        invariant sorted(merged)  // 循环过程中merged始终保持有序
        invariant i < |left| ==> (merged == [] || left[i] >= merged[|merged| - 1])  // 剩余left的首元素不小于merged末尾
        invariant j < |right| ==> (merged == [] || right[j] >= merged[|merged| - 1])  // 剩余right的首元素不小于merged末尾
    {
        if left[i] < right[j] {
            merged := merged + [left[i]];
            i := i + 1;
        } else {
            merged := merged + [right[j]];
            j := j + 1;
        }
    }
    
    assert sorted(merged);
    if i < |left| {
        assert sorted(left[i..]);
        assert merged == [] || left[i] >= merged[|merged| - 1];
        merged := merged + left[i..];
    }
    if j < |right| {
        assert sorted(right[j..]);
        assert merged == [] || right[j] >= merged[|merged| - 1];
        merged := merged + right[j..];
    }
    
    return merged;
}

修改的作用说明 #

• sorted(merged)：直接声明循环每一步中merged都是有序的，Dafny会自动验证每次添加元素后该条件依然成立。
• 剩余元素与merged末尾的关系不变量：保证待合并的left/right剩余部分的首元素不小于当前merged的最后一个元素，结合原left/right本身有序的前提，拼上剩余子序列后整个merged依然有序。
• 合并前的断言：给Dafny的自动验证器明确提示剩余子序列的有序性和大小关系，避免因自动推理能力不足导致验证卡壳。

内容的提问来源于stack exchange，提问作者hyena