如何在Dafny中证明迭代算法保留元素相对顺序？

以下是一段提取整数数组中偶数的Dafny迭代算法，代码已可验证，但缺少输入中偶数元素相对顺序保留的证明（例如FindEvenNumbers([1,2,3,4])应返回[2,4]而非[4,2]）：

predicate IsEven(n: int)
{
    n % 2 == 0
}

method FindEvenNumbers(arr: array<int>) returns (evenNumbers: array<int>)
    // 输入中的所有偶数都在输出中
    ensures forall x :: x in arr[..] && IsEven(x) ==> x in evenNumbers[..];
    // 不在输入中的数也不会出现在输出中
    ensures forall x :: x !in arr[..] ==> x !in evenNumbers[..]
    // 需补充：偶数元素的相对顺序被保留 ???
{
    var evenList: seq<int> := [];
    for i := 0 to arr.Length
        invariant 0 <= i <= arr.Length
        invariant 0 <= |evenList| <= i
        invariant forall x :: x in arr[..i] && IsEven(x) ==> x in evenList[..]
        invariant forall x :: x !in arr[..i] ==> x !in evenList
    {
        if IsEven(arr[i])
        {
            evenList := evenList + [arr[i]];
        }
    }

    evenNumbers := new int[|evenList|](i requires 0 <= i < |evenList| ==> evenList[i]);
    assert evenList == evenNumbers[..];
}

尝试添加循环不变式证明顺序保留未成功，随后用递归filter函数实现了可验证版本，但该版本替换了原迭代算法且filter成为公共API。现针对两个问题解答：

1. 如何在不修改原迭代算法的前提下证明其保留元素相对顺序？ #

无需修改迭代逻辑，只需补充刻画顺序对应关系的循环不变式，并完善方法的后置条件：

步骤1：添加循环不变式 #

在for循环的invariant列表中加入以下条款，直接明确evenList是arr前i个元素中偶数按原顺序组成的序列：

invariant evenList == [x for x in arr[..i] if IsEven(x)]

该不变式的含义是：evenList等价于对arr的前i个元素做顺序过滤（仅保留偶数）的结果，天然保证了顺序一致性。

步骤2：完善方法后置条件 #

在方法的ensures中补充顺序保留的规约：

ensures evenNumbers[..] == [x for x in arr[..] if IsEven(x)]

原理说明 #

循环结束时i == arr.Length，此时evenList == [x for x in arr[..] if IsEven(x)]，结合代码末尾的assert evenList == evenNumbers[..]，Dafny可自动推导出输出数组的元素顺序与输入中偶数的顺序完全一致。

如果不想用序列推导式，也可以用基于位置的逻辑不变式（更繁琐但等价）：

invariant forall j, k: int :: 
    0 <= j < k < i && IsEven(arr[j]) && IsEven(arr[k]) ==>
    exists p, q: int :: 
        0 <= p < q < |evenList| && evenList[p] == arr[j] && evenList[q] == arr[k]

该不变式直接约束：输入前i个元素中任意两个先出现的偶数，在evenList中也保持先出现的顺序。

2. 递归版本是否真正证明了元素相对顺序被保留？ #

递归版本可以真正证明顺序保留，但取决于递归实现的规约是否明确：

典型递归filter实现及规约 #

如果递归filter的实现如下，并附带明确的后置条件：

method filter(s: seq<int>) returns (res: seq<int>)
    ensures res == [x for x in s if IsEven(x)]
{
    if s == [] {
        return [];
    } else {
        var rest := filter(s[1..]);
        if IsEven(s[0]) {
            return [s[0]] + rest;
        } else {
            return rest;
        }
    }
}

证明逻辑 #

递归的核心是保持首元素的相对位置：若首元素是偶数，则将其放在结果的最前面，再拼接剩余部分的过滤结果；若不是，则直接返回剩余部分的过滤结果。这种实现天然遵循原序列的顺序，再配合ensures res == [x for x in s if IsEven(x)]的规约，Dafny可以通过归纳法证明递归结果完全保留原序列中偶数的相对顺序。

但如果递归版本仅声明了元素的存在性（如“输出包含所有偶数”），未明确序列顺序的规约，则无法证明顺序保留。

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