Dafny代码验证问题：MoveZeroesToEnd方法验证失败与超时

原始MoveZeroesToEnd方法验证失败 #

我尝试证明以下Dafny代码，但无法通过验证：

method MoveZeroesToEnd(arr: array<int>)
    requires arr.Length >= 2
    modifies arr
    // 数组长度不变
    ensures arr.Length == old(arr.Length)
    // 第一个零右侧全为零
    ensures forall i, j :: 0 <= i < j < arr.Length && arr[i] == 0 ==> arr[j] == 0
    // 最终数组是原数组的排列
    ensures multiset(arr[..]) == multiset(old(arr[..]))
    // 非零元素相对顺序保留
    ensures forall n, m /* 原数组索引 */:: 0 <= n < m < arr.Length && old(arr[n]) != 0 && old(arr[m]) != 0 ==> 
            exists k, l /* 新数组索引 */:: 0 <= k < l < arr.Length && arr[k] == old(arr[n]) && arr[l] == old(arr[m])
    //ensures IsOrderPreserved(arr[..], old(arr[..]))
    // 零的数量不变
{
    var i := 0;
    var j := 0;

    assert 0 <= i  <= arr.Length;
    assert forall k :: 0 <= k < arr.Length ==> arr[k] == old(arr[k]);
    //assert(forall n, m :: 0 <= n < m < arr.Length  ==> arr[n] == old(arr[n]) && arr[m] == old(arr[m]));
    while j < arr.Length
        invariant 0 <= i <= j <= arr.Length
        // j右侧元素未被修改
        invariant forall k :: j <= k < arr.Length ==> old(arr[k]) == arr[k]
        // i左侧全为非零元素
        invariant forall k :: 0 <= k < i ==> arr[k] != 0
        // i到j（不含j）之间全为零
        invariant forall k :: i <= k < j ==> arr[k] == 0
        // j左侧的零都在i右侧
        invariant forall k :: 0 <= k < j && arr[k] == 0 ==> k >= i
        // j左侧的元素都来自原数组j左侧
        invariant forall k :: 0 <= k < j && arr[k] != old(arr[k]) ==> exists l :: 0 <= l < j && arr[k] == old(arr[l])
        // j左侧子数组是原数组j左侧子数组的排列
        invariant multiset(arr[..j]) == multiset(old(arr[..j]))
        // 非零元素相对顺序在j左侧保留
        invariant forall n, m /* 原数组索引 */:: 0 <= n < m < j && old(arr[n]) != 0 && old(arr[m]) != 0 ==> 
            exists k, l /* 新数组索引 */:: 0 <= k < l < i && arr[k] == old(arr[n]) && arr[l] == old(arr[m])
    {

        if arr[j] != 0
        {
            if i != j
            {
                assert(arr[j] != 0);
                swap(arr, i, j);
                assert(forall k :: 0 <= k <= j ==> exists l :: 0 <= l <= j && arr[k] == old(arr[l]));
            }
            i := i + 1;
        }
        j := j + 1;
    }
    assert j == arr.Length;
}

method swap(arr: array<int>, i: int, j: int)
    requires arr.Length > 0
    requires 0 <= i < arr.Length && 0 <= j < arr.Length
    modifies arr
    ensures arr[i] == old(arr[j]) && arr[j] == old(arr[i])
    ensures forall k :: 0 <= k < arr.Length && k != i && k != j ==> arr[k] == old(arr[k])
{
        var tmp := arr[i];
        arr[i] := arr[j];
        arr[j] := tmp;
}

遇到的问题：

• 第三个后置条件ensures multiset(arr[..]) == multiset(old(arr[..]))在返回路径验证失败，尽管它作为循环不变式成立，且末尾断言assert j == arr.Length;也成立
• 添加额外断言时，验证器会超时。用assume false技术定位到了导致超时的断言，但不知如何修复
• 移除while循环前的两个断言中的任意一个，会出现超时问题
• 注释第三个后置条件，同样会出现超时

我哪里出错了？该如何重写这个证明？

更新：filter函数与SameSequence引理证明尝试 #

遵循避免嵌套存在量词的建议后，我认为需要证明以下内容：

function filter<T>(s: seq<T>, p: T -> bool) : seq<T>
  ensures forall x :: x !in s ==> x !in filter(s, p)
  ensures forall x :: x in s && p(x) ==> x in filter(s, p)
{
  if s == [] then []
  else if p(s[0]) then [s[0]] + filter(s[1..], p)
                  else filter(s[1..], p)
}

// 证明向两个序列添加同一元素时，过滤后的序列保持对应关系
lemma SameSequence<T>(original: seq<T>, filtered: seq<T>,  i: T, p: T -> bool) 
    requires filtered == filter(original, p)
    requires p(i)
    ensures filtered + [i] == filter(original + [i], p)
{
// ???
}

我开始编写这个引理，但过程变得非常复杂，或许我忽略了某些显而易见的点。

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