引理和归纳
# 引理和归纳
# 引言
有时需要一些逻辑步骤来证明一个程序是正确的，但是对于Dafny来说，这些步骤太复杂了。当这种情况发生时，我们通常可以通过提供引理来帮助Dafny证明程序。
引理是用来证明另一个结果的定理，而不是用来证明本身。他们允许Dafny将证明分成两部分:证明引理，然后用引理来证明最终结果;最后的结果就是程序正确性的证明。通过这样分割它，你可以防止Dafny试图证明远超它证明能力的程序。总的来说，Dafny和计算机在处理一堆具体细节情况方面都做得很好，但它缺乏看到能使证明过程变得更容易的中间步骤的能力。
通过使用引理，你可以找出这些中间步骤是什么，以及什么时候在程序使用它们。对于有关归纳论证的问题来说，lemma无疑是对症下药的一剂良方。
# 零搜索
我们首次接触引理，先来学习一个简单的例子:在数组中搜索零。这个问题有趣在于我们正在搜索的这个数组有两个特殊的属性: 所有元素都是非负的。 每个连续元素最多比前一个元素小一。 在代码:
method FindZero(a: array<int>) returns (index: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
{
}
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
2
3
4
5
6
7
有这样的一堆要求条件，我们可以用一些聪明的方法:我们可以跳过元素。假设我们正在遍历数组，看到a[j] == 7。然后我们知道6 <= a[j+1]，5 <= a[j+2]，等等。事实上，下一个0要等到数组中7个元素全部走一遍时才会出现。所以我们甚至不需要刻意寻找0只用一直a[j+a[j]]就行了。所以我们可以这样写一个循环:
method FindZero(a: array<int>) returns (index: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0
ensures 0 <= index ==> index < a.Length && a[index] == 0
{
index := 0;
while index < a.Length
invariant 0 <= index
invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0
{
if a[index] == 0 { return; }
index := index + a[index];
}
index := -1;
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
index := 0;
while index < a.Length
invariant 0 <= index
invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0
{
if a[index] == 0 { return; }
index := index + a[index];
}
index := -1;
2
3
4
5
6
7
8
9
这段代码将计算得到正确的结果，但是Dafny在第二个循环不变量报错。Dafny并不认为跳过所有这些元素是合理的。原因是，前置条件说的是：每个连续的元素最多减一，但它没有说间隔更远的元素是如何关联的。为了让Dafny相信这事实，我们需要使用引理。
# 引理
引理其实就是个ghost方法。引理(更准确地说，引理的结论)所要求的性质被声明为后置条件，就像在普通方法声明的一样。与方法不同，引理永远不会被改变状态。因为引理是ghost方法，所以不需要在运行时调用它，所以编译器在生成可执行代码之前会删除、无视它。因此，引理的存在仅仅是因为它对程序验证有一定作用。一个典型的引理长这样的:
lemma Lemma(...)
ensures (desirable property)
{
...
}
2
3
4
5
对于零搜索问题，理想的性质是在index + a[index]之前，index中的元素都不能为零。按照FindZero的requierments，我们将数组和起始索引作为参数:
lemma SkippingLemma(a: array<int>, j: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
requires 0 <= j < a.Length
ensures forall i :: j <= i < j + a[j] && i < a.Length ==> a[i] != 0
{
//...
}
lemma SkippingLemma(a: array<int>, j: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
requires 0 <= j < a.Length
ensures forall i :: j <= i < j + a[j] && i < a.Length ==> a[i] != 0
{
...
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
后置条件就是我们想要的属性。i有额外限制是因为j + a[j]可能超过了数组的末尾。我们只想讨论这个范围内的下标也就是数组中的下标。然后我们做了一个关键的步骤:检查我们的引理是否足以证明循环不变量。通过在填充引理体之前进行检查，我们确保我们试图证明的是正确的东西。FindZero方法变成:
lemma SkippingLemma(a: array<int>, j: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
requires 0 <= j < a.Length
ensures forall i :: j <= i < j + a[j] && i < a.Length ==> a[i] != 0
{
//...
}
method FindZero(a: array<int>) returns (index: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0
ensures 0 <= index ==> index < a.Length && a[index] == 0
{
index := 0;
while index < a.Length
invariant 0 <= index
invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0
{
if a[index] == 0 { return; }
SkippingLemma(a, index);
index := index + a[index];
}
index := -1;
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
index := 0;
while index < a.Length
invariant 0 <= index
invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0
{
if a[index] == 0 { return; }
SkippingLemma(a, index);
index := index + a[index];
}
index := -1;
2
3
4
5
6
7
8
9
10
现在，Dafny没有报错FindZero方法，因为引理的后置条件显示循环不变式被保留了。但它对引理本身报错，这并不奇怪，因为主体是空的。为了让Dafny接受引理，我们必须证明后置条件为真。就像我们在Dafny中做的所有事情一样:编写代码。
我们从数组的关键属性开始，因为零搜索问题中的元素都只会缓慢下降。我们可以通过使用断言来询问某些属性是否存在。例如，我们可以看到Dafny知道:
lemma SkippingLemma(a: array<int>, j: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
requires 0 <= j < a.Length - 3
// Note: the above has been changed so that the array indices below are good.
{
assert a[j ] - 1 <= a[j+1];
assert a[j+1] - 1 <= a[j+2];
assert a[j+2] - 1 <= a[j+3];
// therefore:
assert a[j ] - 3 <= a[j+3];
}
2
3
4
5
6
7
8
9
10
11
12
assert a[j ] - 1 <= a[j+1];
assert a[j+1] - 1 <= a[j+2];
assert a[j+2] - 1 <= a[j+3];
// therefore:
assert a[j ] - 3 <= a[j+3];
2
3
4
5
因此，我们可以看到，Dafny可以跟随任何单独的步骤，甚至可以适当地链。但是我们需要的步数不是恒定的:它可能取决于a[j]的值。但是我们已经有了一个用于处理可变数量步骤的构造:while循环!
我们可以用同样的结构让Dafny把步骤连在一起。我们想要从j迭代到j + a[j]，同时跟踪下界。我们还会跟踪到我们目前看到的所有元素都不为零的事实:
lemma SkippingLemma(a: array<int>, j: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
requires 0 <= j < a.Length
ensures forall k :: j <= k < j + a[j] && k < a.Length ==> a[k] != 0
{
var i := j;
while i < j + a[j] && i < a.Length
invariant i < a.Length ==> a[j] - (i-j) <= a[i]
invariant forall k :: j <= k < i && k < a.Length ==> a[k] != 0
{
i := i + 1;
}
}
method FindZero(a: array<int>) returns (index: int)
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]
ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0
ensures 0 <= index ==> index < a.Length && a[index] == 0
{
index := 0;
while index < a.Length
invariant 0 <= index
invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0
{
if a[index] == 0 { return; }
SkippingLemma(a, index);
index := index + a[index];
}
index := -1;
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
var i := j;
while i < j + a[j] && i < a.Length
invariant i < a.Length ==> a[j] - (i-j) <= a[i]
invariant forall k :: j <= k < i && k < a.Length ==> a[k] != 0
{
i := i + 1;
}
2
3
4
5
6
7
第一个不变式给出当前元素的边界，如果我们还没有跑到数组的末尾。对于超过j的每一个索引(其中有i-j)，数组元素可以小一，因此从a[j]中减去这个值。这只是说当前元素不能为零，所以如果没有第二个不变量，Dafny就不能知道数组里没有零。Dafny忘记了循环执行的所有内容，除了在不变量中给出的内容，所以我们需要建立这样一个事实，即到目前为止，任何地方都没有零。
循环体只是使计数器加1。正如我们之前看到的，Dafny能够自己计算出每一步，所以我们不需要做任何进一步的操作。我们只需要给它一个需要证明的结构。有时，单个步骤本身就足够复杂到它们需要自己的子证明，通过使用一系列断言语句或整个其他引理。
在使用数组时，迭代是许多问题的自然解决方案。但是，有时会使用递归来定义函数或属性。在这些情况下，引理通常具有相同的递归结构。为了看一个例子，我们将考虑计数的问题。
# 计数
我们将使用count函数在一个bool序列中计算true的数量，如下所示:
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
method m()
{
assert count([]) == 0;
assert count([true]) == 1;
assert count([false]) == 0;
assert count([true, true]) == 2;
}
2
3
4
5
6
7
8
9
10
11
12
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
...
assert count([]) == 0;
assert count([true]) == 1;
assert count([false]) == 0;
assert count([true, true]) == 2;
...
2
3
4
5
6
7
8
9
10
11
代码非常简单，但需要注意的一点是，该函数是递归定义的。像这样的递归函数很容易需要引理。我们希望在验证使用此函数的程序时能够使用count的一个属性:它应用于加法上。我们的意思是:
forall a, b :: count(a + b) == count(a) + count(b)
这里，第一个加号(+)是序列拼接，第二个加号是整数相加。显然，我们可以将任意序列分解为两个序列a和b，分别计算它们，并将结果相加。这是事实，但Dafny无法直接证明。问题是函数并没有以这种方式分割序列。该函数取第一个元素，计算其计数，然后将其添加到序列的其余部分。如果a很长，那么在这个展开过程实际到达count(b)之前可能需要一段时间，因此Dafny只尝试展开几个递归调用。(确切地说，是两个。参见Amin, Leino, and Rompf的论文Computing with an SMT solver, TAP 2014。)这是一个需要引理来证明的性质的例子。
在我们的例子中,我们有两个选择引理:我们也可以写全称量词,或者我们可以使引理特定序列a和b。事实证明,当我们想要分配律,我们不需要完整的通用属性。我们感兴趣的是，对于程序中已知的两个特定的a和b, count(a + b) == count(a) + count(b)。因此，当我们调用引理来得到这个性质时，我们可以告诉它我们感兴趣的是哪两个序列。如果我们在其他地方有不同的序列，我们可以用不同的参数调用方法，就像普通方法一样。事实证明，证明完整的全称性质，虽然是可能的，但比证明具体的，具体的情况要复杂得多，所以我们先来处理这个情况。
因此引理应该将感兴趣的序列作为参数，后置条件如下:
lemma DistributiveLemma(a: seq<bool>, b: seq<bool>)
ensures count(a + b) == count(a) + count(b)
{
}
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
2
3
4
5
6
7
8
9
lemma DistributiveLemma(a: seq<bool>, b: seq<bool>)
ensures count(a + b) == count(a) + count(b)
{
}
2
3
4
# 证明分配性质
为了写出引理，我们必须想出一个证明它的方法。正如您可以在上面验证的(没有双关语)，引理还不能工作，否则引理将是不必要的。为了做到这一点，我们注意到Dafny无法首先证明这一点的原因是count函数从序列的开始定义，而分配律则在序列的中间操作。因此，如果我们能找到一种从序列的前面开始工作的方法，那么Dafny就可以直接使用函数的定义。这个序列的第一个元素是什么?在一些情况下，a和b是空序列(如果有的话)。因此我们的引理必须考虑多种情况，引理的共同特征。我们注意到，如果a ==[]，那么a+ b == b，不管b是多少。引理处理情况的方式与代码处理情况的方式相同:if语句。下面使用断言给出了所需属性的简短证明。
lemma DistributiveLemma(a: seq<bool>, b: seq<bool>)
ensures count(a + b) == count(a) + count(b)
{
if a == []
{
assert a + b == b;
assert count(a) == 0;
assert count(a + b) == count(b);
assert count(a + b) == count(a) + count(b);
}
else
{
//...
}
}
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
if a == []
{
assert a + b == b;
assert count(a) == 0;
assert count(a + b) == count(b);
assert count(a + b) == count(a) + count(b);
}
else
{
...
}
2
3
4
5
6
7
8
9
10
11
在这种情况下，我们可以通过添加一个requires子句来检验引理。我们发现代码验证。这意味着如果a ==[]，则引理将正确地证明后置条件。在这种情况下，只需要上面的第一个断言;Dafny自己完成了剩下的步骤(试试吧!)现在我们可以考虑另一种情况，当0 < |a|。
我们的目标是将count(a + b)与count(a)和count(b)联系起来。如果a不是空序列，那么当我们按照定义展开count(a + b)时，我们得到:
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
method m2(a: seq<bool>, b:seq<bool>)
requires |a| > 0
{
assert a + b == [a[0]] + (a[1..] + b);
assert count(a + b) == count([a[0]]) + count(a[1..] + b);
}
2
3
4
5
6
7
8
9
10
11
assert a + b == [a[0]] + (a[1..] + b);
assert count(a + b) == count([a[0]]) + count(a[1..] + b);
2
注意，我们得到count([a[0]])和a[1..]。如果我们扩展count(a)，这两项也会出现。具体地说:
method m2(a: seq<bool>, b:seq<bool>)
requires |a| > 0
{
assert count(a) == count([a[0]]) + count(a[1..]);
}
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
2
3
4
5
6
7
8
9
10
assert count(a) == count([a[0]]) + count(a[1..]);
最后，我们可以将count(a)的定义替换为后置条件，以获得:
assert count(a + b) == count(a) + count(b); // postcondition
assert count(a + b) == count([a[0]]) + count(a[1..]) + count(b);
2
现在这看起来很像我们展开count(a + b)后得到的表达式。唯一的区别是count(a[1.. .) + count(a[1..]) + count(b)。但这正是我们要证明的性质!
# 归纳
我们试图提出的论点是归纳的。我们可以证明我们的目标，只要这个问题的一个小版本是正确的。这正是归纳法的概念:用一个小问题来证明一个大问题。为此，我们在代码中调用递归属性。它是一个方法，所以我们可以在需要它的时候调用它。
Dafny将假定递归调用满足规范。这就是归纳假设，所有引理的递归调用都是有效的。这关键取决于Dafny也证明了终止。这意味着最终，引理不会再进行递归调用。在本例中，这是if语句的第一个分支。如果没有递归调用，那么引理必须直接证明这种情况。然后，堆栈中的每个调用都是合理的，假设引理适用于较小的情况。如果Dafny没有证明链终止，那么链可以永远继续，并且对于每个调用的假设都是不合理的。
归纳法通常是寻找一种方法，一步一步地建立你的目标。从另一个角度来看，它证明了你的目标是一个更小的版本。通过一次分解一个元素，直到第一个序列完全消失，证明了分配引理。这种情况被证明是一个基本情况，然后整个链的解构被验证。
成功的关键是Dafny从来不用考虑整个通话链。通过检验终止，得到链是有限的。然后它要做的就是检查一步。如果任意一步是有效的，那么整个链也是有效的。这与Dafny在循环中使用的逻辑相同:检查初始不变项是否成立，任意一个步骤是否保持不变，然后检查整个循环，不管循环循环了多少次。这种相似性不仅仅是表面的。这两种引理(以及Dafny对程序的两种推理)都是归纳的。考虑到迭代和递归作为实现同一目标的两种方法之间的关系，这也不足为奇。
记住这一点，我们可以通过在if语句的else分支中递归地调用引理来完成引理:
lemma DistributiveLemma(a: seq<bool>, b: seq<bool>)
ensures count(a + b) == count(a) + count(b)
{
if a == []
{
assert a + b == b;
}
else
{
DistributiveLemma(a[1..], b);
assert a + b == [a[0]] + (a[1..] + b);
}
}
function count(a: seq<bool>): nat
{
if |a| == 0 then 0 else
(if a[0] then 1 else 0) + count(a[1..])
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
if a == []
{
assert a + b == b;
}
else
{
DistributiveLemma(a[1..], b);
assert a + b == [a[0]] + (a[1..] + b);
}
2
3
4
5
6
7
8
9
现在这个引理得到了验证。但是如果我们想要表达每一对序列都是这样联系的呢?为了做到这一点，我们必须看看引理在Dafny中的另一种用法，我们将用另一个例子来探索。
# 有向图的路径
作为最后一个更高级的例子，我们将证明一个关于有向图中路径的性质。为此，我们有机会称一个引理在所有节点序列上是普遍的。一个有向图由若干个节点组成，每个节点都有一些到其他节点的链接。这些链接是单向的，对它们的唯一限制是节点不能链接到自己。节点定义为:
class Node
{
// a single field giving the nodes linked to
var next: seq<Node>
}
2
3
4
5
我们将图表示为一组节点，这些节点只指向图中的其他节点，而不指向自己。我们称这样一组节点为封闭的:
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph ==>
forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i
}
2
3
4
5
6
我们将路径表示为非空节点序列，其中每个节点都与路径中的前一个节点相连。我们定义了两个谓词，一个用于定义有效路径，另一个用于确定给定路径是否为图中两个特定节点之间的有效路径:
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
现在我们准备好陈述我们要证明的引理了。我们考虑一个图和一个子图:一个也构成一个图的节点的子集。这个子图必须是封闭的，即不包含自身之外的链接。如果我们有这样的情况，那么从子图中的一个节点到子图之外的一个节点不可能有一条有效的路径。我们将这个事实称为闭合引理，我们在Dafny中这样表述:
lemma ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph))
{
//...
}
class Node
{
var next: seq<Node>
}
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph ==> forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i
}
lemma ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph))
{
...
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
前提条件说明了所有的要求:图和子图都是有效的，根节点在子图中但目标不在，所有内容都包含在主图中。后置条件声明没有从根到目标的有效路径。这里我们只对特定的开始/结束节点对证明它。
证明某物不存在的一种方法是证明给定的任意节点序列它不是一个有效路径。我们可以用，你猜对了，另一个引理。这个引理将证明，对于任何给定的序列，它不是从根root到目标goal的有效路径。路径引理的反证如下:
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !pathSpecific(p, root, goal, graph)
{
}
class Node
{
var next: seq<Node>
}
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph ==> forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !pathSpecific(p, root, goal, graph)
{
...
}
2
3
4
5
6
7
8
前提与闭引理相同。要在闭引理ClosedLemma中使用反证明引理DisproofLemma，我们需要对每个节点序列调用它一次。这可以通过Dafny的forall语句来完成，该语句聚合了给定绑定变量的所有值对其主体的影响。
lemma ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph))
{
forall p {
DisproofLemma(p, subgraph, root, goal, graph);
}
}
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !pathSpecific(p, root, goal, graph)
{
}
class Node
{
var next: seq<Node>
}
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph =
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
lemma ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)
...
ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph))
{
forall p {
DisproofLemma(p, subgraph, root, goal, graph);
}
}
2
3
4
5
6
7
8
如你所见，这使得闭引理ClosedLemma得到验证，所以我们对引理的测试是成功的。因此，反证明引理DisproofLemma是足够强的，我们的工作仅仅是证明它。
有几种不同的方式可以使节点序列成为无效路径。如果路径为空，则它不能是有效路径。此外，路径的第一个元素必须是根root，最后一个元素必须是目标goal。因为root in subgraph，goal !in subgraph，我们必须有root != goal，所以序列必须至少有两个元素。为了验证Dafny是否看到了这一点，我们可以临时在引理上加上先决条件，如下所示:
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
requires |p| < 2 || p[0] != root || p[|p|-1] != goal
ensures !pathSpecific(p, root, goal, graph)
{
}
class Node
{
var next: seq<Node>
}
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph ==> forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires ... // as before
requires |p| < 2 || p[0] != root || p[|p|-1] != goal
...
{
}
2
3
4
5
6
7
注意，这将导致闭引理ClosedLemma停止验证，因为引理现在只对一些序列有效。我们将忽略闭合引理ClosedLemma，直到我们完成反驳引理DisproofLemma。这就证明了，这意味着Dafny能够在这些情况下证明后置条件。因此，我们只需要证明当这些条件不成立时，路径是无效的。我们可以用if语句来表达:
if 1 < |p| && p[0] == root && p[|p|-1] == goal {
(further proof)
}
2
3
如果路径至少有两个元素长，第一个元素是根root元素，最后一个元素是目标goal元素，那么我们就有了进一步的证明。如果这些条件没有满足(也就是说，如果if语句的保护为false，并且控制在隐式else分支中继续)，Dafny将自己证明后置条件(高级备注:你可以通过临时添加语句assume false来检查这一点;在if的then分支中)。现在我们只需要填入进一步的证明部分。在这样做时，我们可以假定if语句的保护条件。我们现在可以使用和上面一样的归纳技巧。
如果序列从根root节点开始，并在目标节点goal结束，则它不能有效，因为序列必须在某个点上有一个不在前一个节点下一个列表中的节点。当我们得到任何像这样的特定序列时，我们可以将它分为两种情况:要么序列在从第一个节点到第二个节点的链接中无效，要么它在一行中的某个地方被打断了。就像在计数示例中一样，Dafny可以看到，如果第一个到第二个节点链接无效，那么序列就不能是路径，因为这反映了路径path的定义。因此，只有当第一个链接有效时，我们才有进一步的工作要做。我们可以用另一个if语句来表达:
if 1 < |p| && p[0] == root && p[|p|-1] == goal {
if p[1] in p[0].next {
(yet further proof)
}
}
2
3
4
5
这里是归纳induction。我们知道p[0] == root, p[1] in p[0].next.中。我们还从子图的根root in subgraph的先决条件知道。因此，由于闭子图 closed(subgraph)，我们知道p[1] in subgraph 。这些条件和我们开始时是一样的!我们现在面对的是同一个问题的一个小版本。我们可以递归地调用反证明引理DisproofLemma来证明p[1..不是一条路。这意味着，根据路径path的定义，p不能是路径，并且满足第二个后置条件。这可以实现为:
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !pathSpecific(p, root, goal, graph)
{
if 1 < |p| && p[0] == root && p[|p|-1] == goal {
if p[1] in p[0].next {
DisproofLemma(p[1..], subgraph, p[1], goal, graph);
}
}
}
lemma ClosedLemma(subgraph: set<Node>, root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !(exists p: seq<Node> :: pathSpecific(p, root, goal, graph))
{
forall p {
DisproofLemma(p, subgraph, root, goal, graph);
}
}
class Node
{
var next: seq<Node>
}
predicate pathSpecific(p: seq<Node>, start: Node, end: Node, graph: set<Node>)
requires closed(graph)
reads graph
{
0 < |p| && // path is nonempty
start == p[0] && end == p[|p|-1] && // it starts and ends correctly
path(p, graph) // and it is a valid path
}
predicate path(p: seq<Node>, graph: set<Node>)
requires closed(graph) && 0 < |p|
reads graph
{
p[0] in graph &&
(|p| > 1 ==> p[1] in p[0].next && // the first link is valid, if it exists
path(p[1..], graph)) // and the rest of the sequence is a valid
}
predicate closed(graph: set<Node>)
reads graph
{
forall i :: i in graph ==> forall k :: 0 <= k < |i.next| ==> i.next[k] in graph && i.next[k] != i
}
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
lemma DisproofLemma(p: seq<Node>, subgraph: set<Node>,
root: Node, goal: Node, graph: set<Node>)
requires closed(subgraph) && closed(graph) && subgraph <= graph
requires root in subgraph && goal in graph - subgraph
ensures !pathSpecific(p, root, goal, graph)
{
if 1 < |p| && p[0] == root && p[|p|-1] == goal {
if p[1] in p[0].next {
DisproofLemma(p[1..], subgraph, p[1], goal, graph);
}
}
}
2
3
4
5
6
7
8
9
10
11
12
现在闭引理DisproofLemma被验证了，随着测试前提的移除，我们看到闭引理ClosedLemma也被验证了。由此证明了封闭子图不存在从内部到外部的路径。
当一个引理需要无限次实例化时，forall语句是有用的。这个例子展示了forall语句的一个简单版本。要了解更高级的版本，请参见Leino的《Dafny中的良好基础函数和极端谓词:教程》，iwill -2015，或Dafny测试套件中的示例。
永远记得检查你的引理是否足以证明你需要的。没有什么比花时间做引理验证，结果发现你需要更强大的东西更令人沮丧的了。这也可以让你避免创建一个带有前置条件的引理，因为前置条件的限制太大，以至于你不能在需要的地方调用它。