2

这是一个简单的 Dafny 程序：两行代码和三个断言。

method Main()
{
    var S := set s: int | 0 <= s < 50 :: 2 * s;
    var T := set t | t in S && t < 25;
    assert |S| == 50;                    // does not verify  
    assert T <= S;                       // does verify
    assert T < S;                        // does not verify
}

S 的基数是 50，但 Dafny 无法验证此声明，如所写。同样，T 显然是 S 的一个子集，而 Dafny 可以验证这一说法；但 T 也是 S 的真子集，Dafny 无法验证这一说法。

导致这些困难的“幕后”发生了什么？学习和使用 Dafny 的人是否可以预见并避免或处理这些困难？

4

1 回答 1

2

Dafny 无法验证第一个断言，因为 Dafny 没有用于推理集合推导的基数的内置模型。所以它永远无法像|S| == 50自己那样证明方程。然而，它可以推断一些其他集合操作的基数，例如联合和单例集合。您可以使用它以一种相当迂回的方式说服 Dafny，|S| == 50我将在下面展示。

Dafny 无法证明最后一个断言，因为它不够聪明，无法提出一个S不在T. 我们可以通过提到这样一个元素来帮助它。更多关于下面的内容。

设置适当的触发器

但首先，有一个关于集合理解的警告，说 Dafny“找不到任何触发条件”。这与 Dafny 如何使用量词将集合理解转换为一阶逻辑有关。Dafny 指示 Z3 使用某些句法模式（称为触发器）来推理量词，但此警告表示找不到这样的模式。这个问题不仅仅是抽象的，达夫尼在推理这种理解时遇到了严重的麻烦：它甚至无法证明0 in S。

解决此类问题的一种相当通用的方法是引入一个新函数来缩写公式中可用作触发器的某些部分。具体来说，定义

function method Double(n: int): int {
    2 * n
}

然后将理解改写为

var S := set s: int | 0 <= s < 50 :: Double(s);

这样 Dafny 就可以使用触发器了Double(s)。现在，每当你想说服 Dafny 有什么东西在 中时S，你可以将它作为Double(x)some来提及x，Dafny 将能够证明这一点。

例如，要0 in S在新定义下显示，我们可以说

assert Double(0) in S;  // remove this to see the one below fail
assert 0 in S;

证明T < S

到目前为止，我们所做的只是稍微调整一下程序，以便 Dafny 可以更好地推理S. 这已经足以修复你的最终断言的证明T < S，所以让我们接下来看看。

Dafny 理解T < S为（基本上）T <= S && T != S。你已经看到它能够展示了T <= S，所以它还有待证明T != S。最简单的方法是展示一个集合中不在另一个集合中的元素，在这种情况下，其中的一个元素S不在T. 26 就是这样一个元素，我们可以通过添加行来修复断言

assert Double(13) in S;  // mention the trigger; this proves 26 in S
assert T < S;            // now verifies

证明|S| == 50

最后，让我们回到第一个失败的断言，即|S| == 50. 这个更难修复。可能有一个较短的证明，但我将向您展示一种方法，该方法也可以帮助您了解如何自行解决类似问题。

我们的方法是首先证明S可以用两个更简单的函数表示，然后证明关于这两个函数如何影响基数的引理。

Dafny 能够显示

assert S == MapSet(Double, RangeSet(0, 50));

其中RangeSet(a,b)是构造 和 之间的整数集合的函数a，b并且MapSet是“将函数映射到集合”的函数。这些函数定义如下：

function method RangeSet(a: int, b: int): set<int> {
    set x: int | a <= x < b
}

function method MapSet<A,B>(f: A -> B, S: set<A>): set<B>
{
    set x | x in S :: f(x)
}

因此，为了证明关于 的某些事情|S|，只需推理 的基数RangeSet并证明（在适当的条件下）MapSet保持基数就足够了。这里有两个关于这个效果的引理

lemma CardRangeSet(a: int, b: int)
    requires a <= b
    decreases b - a
    ensures |RangeSet(a, b)| == b - a

lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
    requires Injective(f)
    decreases S
    ensures |MapSet(f, S)| == |S|

CardRangeSeta表示和b之间的数字集的基数b - a，这应该是相当直观的，记住它RangeSet包含a但不包含b。

引理CardMapSetInj说单射函数在映射到集合时保持基数。请注意，这Double是单射的（Dafny 认为这很明显——它不需要证明）。另请注意，单射性假设对于保持引理是必要的，否则如果函数将输入集的两个元素发送到相同的输出元素，映射可能会降低基数。我们可以定义Injective如下：

predicate Injective<A, B>(f: A -> B)
{
    forall x, y :: x != y ==> f(x) != f(y)
}

我将证明下面的两个引理，但首先让我们看看如何使用它们来完成显示|S| == 50。

assert S == MapSet(Double, RangeSet(0, 50));
CardMapSetInj(Double, RangeSet(0, 50));
assert |S| == |RangeSet(0, 50)|;
CardRangeSet(0, 50);
assert |S| == 50;                    // now verifies

还不错！我们首先调用CardMapSetwithDouble来证明|S| == |RangeSet(0, 50)|. 然后我们调用CardRangeSetshow |RangeSet(0, 50)| == 50，它完成了证明。

这两个引理都通过归纳证明。

lemma CardRangeSet(a: int, b: int)
    requires a <= b
    decreases b - a
    ensures |RangeSet(a, b)| == b - a
{
    if a != b {
        calc {
            |RangeSet(a, b)|;
            { assert RangeSet(a, b) == {a} + RangeSet(a + 1, b); }
            |{a} + RangeSet(a + 1, b)|;
            1 + |RangeSet(a + 1, b)|;
            { CardRangeSet(a + 1, b); }
            1 + (b - (a + 1));
            b - a;
        }
    }
}

CardRangeSet由 上的归纳证明b - a。Dafny 发现基本情况微不足道，因此我们只考虑当 时的归纳步骤a != b。证明的工作原理是展开RangeSet以拉出a，然后调用归纳假设(a + 1, b)并进行清理。

（证明是用计算风格写的。如果你不熟悉calc，它可以让你写出非常简洁易读的一系列方程。大括号中的行是证明注释，说明为什么下一行等于前一行. 如果不需要注释，可以省略。有关详细信息，请参阅 Dafny 手册calc。）

lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
    requires Injective(f)
    decreases S
    ensures |MapSet(f, S)| == |S|
{
    if S != {} {
        var x :| x in S;
        calc {
            |MapSet(f, S)|;
            { assert MapSet(f, S) == MapSet(f, {x} + (S - {x})) == {f(x)} + MapSet(f, S - {x}); }
            |{f(x)} + MapSet(f, S - {x})|;
            1 + |MapSet(f, S - {x})|;
            { CardMapSetInj(f, S - {x}); }
            |S|;
        }
    }
}

CardMapSetInj是通过对参数集的归纳证明的S。同样，基本情况是微不足道的，被省略了。在非空的归纳步骤中S，我们选择一个任意元素x in S（这样的元素x存在，因为S它是非空的）。然后我们可以展开MapSeton的定义S并将归纳假设称为 on S - {x}。

（如果您不熟悉语法var x :| x in S，这是 Dafny 的“让这样的”语句。它有点类似于赋值语句，除了不是将特定值分配给x，而是选择满足右侧的谓词:|。在验证过程中，Dafny 验证是否存在这样的元素。程序的其余部分对 的值一无所知，x除非它满足谓词。有关更多详细信息，请参阅 Dafny 参考。）

包起来

这里基本上有两个想法：

  1. 引入新功能作为触发器
  2. 理解有时难以推理；改用函数。

也可能有一种方法可以|S| == 50更直接地证明，方法是引入一个函数，该函数通过返回f(n)来概括定义的理解。然后可以直接通过归纳来证明这一点，然后注意这一点。Sset s | 0 <= s < n :: Double(s)n|f(n)| == nS == f(50)

那将是一个非常好的替代证明，我鼓励您尝试自己开发它。我在这里给出的证明的一个优点是它更通用（如果您经常操作集合，它可能通常很有用）MapSet。RangeSet

于 2018-02-26T13:39:32.230 回答