Dafny 递归按顺序命中每个元素，无法验证

Question

以下函数 seqToSet 接受一个元素序列和 returns 一个包含给定序列中所有（且仅）元素的集合。它通过使用相同的序列和空集调用递归辅助函数 addSeqToSet 来完成此操作。辅助函数将序列中的每个元素添加到给定的集合中，并 returns 结果。它通过对序列的 head/tail 结构进行递归来实现。它在序列为空时完成，否则使用序列的尾部和集合与包含序列头的单例集的并集递归调用自身。

Dafny 无法自行验证表明结果集包含原始序列中所有元素的后置条件。

帮助它看到这种情况的正确策略是什么？

function method seqToSet(q: seq<int>): set<int>
{
    addSeqToSet(q, {})
}

function method addSeqToSet(q: seq<int>, t: set<int>): (r: set<int>)
    ensures forall i :: i in q ==> i in r
{
    if | q | == 0 then t
    else addSeqToSet (q[1..], t + { q[0] })
}

Answer 1

当 Dafny 试图验证递归函数的后置条件时，它通过归纳推理：假设后置条件对任何递归调用都成立，并证明它对当前调用也成立。

想象一下 Dafny 如何推理 addSeqToSet。

在第一个分支中，| q | == 0 意味着 q 是空的，因此后置条件很简单，因为没有元素 i in q.

在第二个分支中，Dafny 假定递归调用的后置条件：

forall i :: i in q[1..] ==> i in r

然后尝试证明当前调用的后置条件：

forall i :: i in q ==> i in r

注意由于addSeqToSet直接returns递归调用的答案，r在上面两个公式中是相同的。

如果你想一想，你会发现外部调用的后置条件不遵循递归调用的后置条件，因为递归调用没有说明 q[0].

您需要以某种方式加强后置条件，以便您也知道 q[0] in r。

这样的强化之一是添加关于 t

的额外后置条件

ensures forall i :: i in t ==> i in r

Dafny 然后验证两个后置条件。

Dafny 递归按顺序命中每个元素，无法验证

Dafny recursion hits every element in sequence, can't verify

dafny