1

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

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] })
}
4

1 回答 1

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直接从递归调用返回答案，因此r在上述两个公式中是相同的。

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

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

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

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

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

于 2018-02-16T23:35:48.497 回答