Dafny
lijiahai
2022-03-25
目录

不同类型的证明

# 不同类型的证明

K. Rustan M. Leino Manuscript KRML 276, 9 March 2020

摘要 就像写作和口语中有不同的句子结构来表达不同的想法一样，也有不同的证明结构来表达证明。这条注释显示了在Dafny中可能出现的一些变化。

让我们考虑不同的证明写作风格。作为一个运行的例子，我们将首先定义一个函数及其行为的一些公理。

# 一个示例问题

考虑一个带有两个参数的整数函数f:

function f(x: int, y: int): int
1

因为我没有为这个函数提供一个函数体，所以Dafny将它视为一个未解释的函数。也就是说我们对它一无所知。我们知道它是一个函数，这意味着它的结果值完全由它的输入决定。例如，我们不知道f(7,3)计算的是哪个整数，但是知道如果你用相同的参数再次调用f，你会继续得到相同的值。

为了证明关于f的一些东西，我们想知道更多关于f的性质。下面是三个引理的声明，它们表达了这样的属性:

lemma Associativity(x: int, y: int, z: int)
  ensures f(x, f(y, z)) == f(f(x, y), z)

lemma Monotonicity(y: int, z: int)
  requires y <= z
  ensures forall w :: f(w, y) <= f(w, z)

lemma DiagonalIdentity(x: int)
  ensures f(x, x) == x
1
2
3
4
5
6
7
8
9

就像函数本身一样，这些引理没有实体。它是引理的主体来证明引理的后置条件。换句话说，主体是证明引理的东西。因为这些引理没有证明，所以它们实际上是“公理”(也就是说，你必须在没有证明的情况下接受它)。

如果你通过Dafny 编译器运行这个函数和这些引理，你会收到抱怨，说它们没有实体。但出于本文的目的，我们并不关心从编译器获取正在执行的代码。我们的重点是证明，而Dafny 验证者对无实体声明没有异议。就验证者而言，无主体声明只是说没有什么可检查的。

我们将以不同的风格来证明这个性质:

a,b, c,和x,如果c < = x = = f (a, b),然后f (a、f (b, c)) < = x。

这个性质的证明使用了上面的三个公理。

# 证明计算

有时，一个简单的“断言”语句就足以提示Dafny验证器完成一个证明。其他时候，您需要调用一个引理。当情况没有这么简单时，在Dafny中编写证明的最常见方法是证明计算 [0 (opens new window)， 3 (opens new window)]。

证明计算是一系列的证明步骤。每一步证明一个等式(例如，A == B)、不等式(例如，A <= B)或逻辑推论(例如，A ==> B)。

一个步骤是垂直书写的，以给一些空间来证明为什么这个步骤是成立的。下面是一个原型步骤:

  A;
==  // explain why A equals B
  B;
1
2
3

如本步骤所示，链中的每个公式都以分号结束。

在上面的原型步骤中，我将理由(也称为hint)作为注释编写。这样的注释是有用的文档。如果验证者不能在没有帮助的情况下检查您的步骤，则提示需要不仅仅是注释。然后，用花括号写一段代码，验证者使用从代码中获得的知识来证明这一步。例如,

  A;
==  { LemmaThatJustifiesABEquality();  }
  B;
1
2
3

是时候写证明了。这里是:

lemma CalculationalStyleProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  calc {
    f(a, f(b, c));
  ==  { Associativity(a, b, c); }
    f(f(a, b), c);
  ==  { assert f(a, b) == x; }
    f(x, c);
  <=  { assert c <= x; Monotonicity(c, x); }
    f(x, x);
  ==  { DiagonalIdentity(x); }
    x;
  }
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

让我们来看看这个证明计算。

第一步说，根据结合律，表达式f(a, f(b, c))等于f(f(a, b)， c)注意，这个提示使用特定参数a， b和c调用结合性引理。

第二步说f(f(a, b)， c)和f(x, c)是一样的，因为我们要证明的引理的前提(即先决条件)说x等于f(a, b)。验证者根据我们要证明的引理的前提知道x == f(a, b)这个等式，所以验证者在这个证明步骤中不需要明确的提示。但是，有时候用机器检查的方式来做这样的语句会很好，你可以用“assert”语句来做，就像我在这里展示的那样。

第三步证明f(x, c) <= f(x, x)。这一步的理由是c <= x保持不变(它是在引理前提条件下给出的)，因此可以将引理称为单调性(这需要c <= x作为前提条件)。调用单调性(c, x)引理给了我们

forall w :: f(w, c) <= f(w, x)
1

验证者指出，用x为w实例化这个量词给出了我们在这一步中试图证明的不等式。

第四步证明了f(x, x) = x。这个属性直接遵循DiagonalIdentity公理，用参数x调用。

我们的四个证明步骤证明了以下四个相应的性质:

f(a, f(b, c)) == f(f(a, b), c)
f(f(a, b), c) == f(x, c)
f(x, c) <= f(x, x)
f(x, x) == x
1
2
3
4

通过==和<=的传递性，这四个性质给了我们

f(a, f(b, c)) <= x
1

这就是我们要证明的。

# 连接和线型计算

一般来说，我发现证明计算是令人信服的，容易阅读。您可以分别检查每一步，并可以看到公式是如何从一行“转换”到一行的。

很多时候(但并非总是如此)，我也发现证明计算对作者来说很简单。在上面的例子中，我们从公式的左边开始计算

f(a, f(b, c)) <= x
1

我们要证明。然后，我们看一下证明的当前行，找出关于这个表达式我们知道什么性质，以及我们接下来可以应用什么变换。为了在这个过程中获得更多的指导，通常最好从我们试图证明的公式的更复杂的一面开始。举个例子，如果你从

calc {
  x;
1
2

现在还远不清楚下一步会怎样

==  { DiagonalIdentity(x); }
  f(x, x);
1
2

我们可以继续这个证明，将上一节的步骤按相反的顺序写下来，并在每一步中反转运算符的方向(例如，将<=更改为>=):

>=  { assert c <= x; Monotonicity(c, x); }
  f(x, c);
1
2

不管我们往哪个方向走，到目前为止，我所展示的计算中的每一行都有类型int。也可以在每一行用一个布尔公式来写证明。这里有一个这样的例子:

calc {
  f(a, f(b, c)) <= x;
==  { DiagonalIdentity(x); }
  f(a, f(b, c)) <= f(x, x);
==  { Associativity(a, b, c); }
  f(f(a, b), c) <= f(x, x);
==  { assert f(a, b) == x; }
  f(x, c) <= f(x, x);
==  { assert c <= x; Monotonicity(c, x); }
  true;
}
1
2
3
4
5
6
7
8
9
10
11

通过==的传递性，证明了公式f(a, f(b, c)) <= x的值为true。

如果您为您的证明计算行选择这样的布尔表达式，那么每一步的操作符通常是逻辑暗示(==>，即“逻辑弱化”)或逻辑“解释”(<==，“逻辑强化”，或“从后”)。当然，你必须选择这两个方向中的一个，而不是同时使用，否则你的证明计算就没有意义了。在这些方向中，<==通常会给你一个更好的起点，因为你会从你要证明的公式开始，最后你会得到true。然而，根据我的经验，我发现许多初学者被<==的方向搞糊涂了，他们把计算写得好像他们是在==>的方向上。用任何对你有意义的方向。

# 最简证明

证明计算是一种构造证明步骤的方法。它通常包含比验证者需要的更多的信息，特别是如果您为了自己的利益，将证明写在小的步骤中。如果你认为一个证明有太多的细节，你可以删除一些不需要的东西。这是否是个好主意——或者，什么时候是个好主意，删除多少内容——主要取决于个人喜好。如果您稍后再回到证明，额外的细节可能会提供有用的文档，说明证明最初是如何构造的。

如果你想减少上面的证明计算中的提示，你可能要做的第一件事是删除作为证明的一部分的两个assert语句，或者至少删除断言c <= x。但是你可以做的更多。

通过前面的计算，我们可以很容易地看到使用了哪些引理，更重要的是，这些引理实例化了哪些值。一旦你知道了这一点，你就可以完全不用计算证明了。整个证明是这样的:

lemma MinimalProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  Associativity(a, b, c);
  Monotonicity(c, x);
  DiagonalIdentity(x);
}
1
2
3
4
5
6
7
8

# 结构化断言

为了说明这一点，不写calc语句的计算证明是有益的。这是它看起来的样子:

lemma AssertProof(a: int, b: int, c: int, x: int)
  requires c <= x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  Associativity(a, b, c);
  assert f(a, f(b, c)) == f(f(a, b), c);

  assert f(a, b) == x;
  assert f(f(a, b), c) == f(x, c);

  assert c <= x; Monotonicity(c, x);
  assert f(x, c) <= f(x, x);

  DiagonalIdentity(x);
  assert f(x, x) == x;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

这四组语句中的每一组都对应于[1]节(http://leino.science/papers/krml276.html#sec-calc)计算中的一个步骤。在这个步骤证明的等式或不等式的断言之前，calc语句的提示是什么?验证者然后把四个结论粘在一起来证明引理的后置条件。

# 作用域

[1]节(http://leino.science/papers/krml276.html#sec-calc)中的calc语句与[4]节(http://leino.science/papers/krml276.html#sec-linear-asserts)中的拆分的assert语句之间存在差异。不同之处在于，计算中的每一个提示对于证明步骤来说都是局部的。也就是说，提示的作用域就是步骤本身。例如，假设您将1 (opens new window)部分中calc语句的所有提示移动到第一个证明步骤。然后，两个证明步骤将不再验证:

calc {
  f(a, f(b, c));
==  { Associativity(a, b, c);
      assert f(a, b) == x;
      assert c <= x; Monotonicity(c, x);
      DiagonalIdentity(x);
    }
  f(f(a, b), c);
==
  f(x, c);
<=  // error: step not verified
  f(x, x);
==  // error: step not verified
  x;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

也就是说，在第一步中调用提示中的三个引理所获得的信息不会影响到其他步骤。相反，如果你收集引理主体开始的提示，四个等式和不等式就可以很好地验证:

// hints
Associativity(a, b, c);
assert f(a, b) == x;
assert c <= x; Monotonicity(c, x);
DiagonalIdentity(x);
// equalities and inequalities
assert f(a, f(b, c)) == f(f(a, b), c);
assert f(f(a, b), c) == f(x, c);
assert f(x, c) <= f(x, x);
assert f(x, x) == x;
1
2
3
4
5
6
7
8
9
10

你可以把calc表述的每一步都看作是一个引理，引理的证明就放在这一步的提示里。这在编写证明时很重要，不仅因为它告诉人类读者某个提示适用于特定的证明步骤，还因为它限制了验证者应用提示的范围。对于复杂的证明，这在实践中会产生很大的不同，因为验证者可能会被太多的信息“弄糊涂”——这表现为验证者的性能差或某些“蝴蝶效应”[2 (opens new window)]。

总之，在证明中区分提示是很好的。calc语句在这方面做得很好，但你也可以用assert语句的形式来做。下面我们来看一下。

# 断言

assert E;表述了三件事:

  1. 它表明你期望条件E成立
  2. 它要求验证者证明E 3.它让后面的断言假设E

您可能没有考虑过将断言的这三个方面分开，但是这样做很有用，因为Dafny提供了(1)和(2)的替代方案。

该声明

assert E by { Hint }
1

改变方面(1)说E是在给定的提示下被证明的，其中hint是一个命题。提示的作用域只是断言本身，所以它在断言的下游不可用。这样，assert by语句等价于:

calc {
  E;
==  { Hint }
  true;
}
1
2
3
4
5

我们可以使用assert by重写4 (opens new window)部分的证明:

assert f(a, f(b, c)) == f(f(a, b), c) by {
  Associativity(a, b, c);
}
assert f(f(a, b), c) == f(x, c) by {
  assert f(a, b) == x;
}
assert f(x, c) <= f(x, x) by {
  assert c <= x; Monotonicity(c, x);
}
assert f(x, x) == x by {
  DiagonalIdentity(x);
}
1
2
3
4
5
6
7
8
9
10
11
12

这提供了更好的分区，从而更直接地表达了为什么每个断言的条件保持不变。

# 原型显性证明

6 (opens new window)部分中的证明包含两个断言，它们重申了在前置条件中所写的内容。这些断言背后的思想是明确使用这些先决条件的地方。然而，这有两个缺点。

一个缺点是，必须将断言中的表达式与证明中的其他表达式进行比较，才能意识到断言只是在重申一个以前可用的假设。如果我们可以标记条件，然后引用标签，那就好了。

另一个缺点是，无论是否在断言中重述条件，前提条件都是可用的。如果我们忘记编写断言(可能是因为我们没有意识到我们依赖于这个条件)，或者如果我们意外地编写了错误的前提条件，那么证明仍然有效。也就是说，验证器已经能够使用前置条件，所以它不关心你是重述条件，还是陈述一个不同的(真)条件，或者什么也不陈述。如果我们能更明确地说明这些假设的范围，那就太好了。

还有一种形式的断言by语句。它放松了[6]部分(http://leino.science/papers/krml276.html#sec-assert-by)的aspect(2)。这个表单看起来像这样:

assert Label: E { Hint }
1

这个有标记的断言语句表示你期望条件E成立，它提供了一个提示语句作为E的证明。在条件前使用标签会抑制“E”作为下游假设的使用。

例如，要证明f(12,12) == 12，需要使用DiagonalIdentity公理。如果你使用带标签的assert by来证明这个事实，那么在带标签的assert之后，被证明的事实仍然不可用:

assert Label: f(12, 12) == 12 by {
  DiagonalIdentity(12);
}
assert f(12, 12) == 12;  // error: assertion not verified
1
2
3
4

如果你不能用你证明的事实，为什么要用这种说法呢?好吧，我应该说事实在标记的断言之后不是“自动”可用的。但是您可以明确地请求它。你可以用“揭示”声明来做到这一点，在声明中你提到了标签。

下面又是一个例子，但带有“reveal”语句:

assert Label: f(12, 12) == 12 by {
  DiagonalIdentity(12);
}
reveal Label;  // this recalls the condition from the prior assertion
assert f(12, 12) == 12;
1
2
3
4
5

你可以在前提条件上使用同样的技巧。也就是说，通常在引理(或方法或函数)中，是一个先决条件

requires E
1

在引理的整个正文中都有。但如果你给它贴上标签，你就必须使用“揭示”语句来引出这个假设:

requires Label: E
1

在我们看到它的实际应用之前，让我先谈谈标签。Dafny中的标签可以是任何标识符，但它也可以是文本上看起来像数字字面量的东西。以下是五个标签示例:

MyLabel    Label57    L57    57    000_057
1

这是五个不同的标签——事实上，“57”和“000_057”作为数字字面量表示相同的数字，并不意味着它们是相同的标签。如果它们在印刷页上看起来不一样，它们就是不同的标签。(对于类中的字段名、数据类型的析构函数和其他类型成员也是如此，它们也具有允许看起来像文字的标识符的扩展语法。)

好了，现在我们准备在运行的例子中使用带标签的断言:

lemma DifferentStyleOfProof(a: int, b: int, c: int, x: int)
  requires A: c <= x
  requires B: x == f(a, b)
  ensures f(a, f(b, c)) <= x
{
  assert 0: f(a, f(b, c)) == f(f(a, b), c) by {
    Associativity(a, b, c);
  }

  assert 1: f(f(a, b), c) == f(x, c) by {
    reveal B;
  }

  assert 2: f(x, c) <= f(x, x) by {
    assert c <= x by { reveal A; }
    Monotonicity(c, x);
  }

  assert 3: f(x, x) == x by {
    DiagonalIdentity(x);
  }

  assert 4: f(a, f(b, c)) == f(x, c) by {
    reveal 0, 1;
  }

  assert 5: f(x, c) <= x by {
    reveal 2, 3;
  }

  assert f(a, f(b, c)) <= x by {
    reveal 4, 5;
  }
}
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
32
33
34

在这种类型的证明中(在一些逻辑学文本中很常见)，每个断言都通过其相关性显式地证明。如果您认为断言之间的依赖关系构成了一个证明DAG，那么这种证明风格就是对DAG中的祖先进行显式的证明。您可以使用嵌套的assert by语句和标记的断言的层次结构来近似lamport风格的证明[1 (opens new window)]。

# 总结

校样的写作风格有很多种。最简单的证明是那些自动完成的，不需要进一步证明的证明。其他简单的证明需要一个断言或引理。证明步骤可以使用calc语句和assert by语句组织。通过标记一个“assert By”语句或一个前置条件，这个条件在证明中被抑制了，直到你使用一个“reveal”语句明确地请求它回来。

构造证明是一个好主意，为了可读性和清晰度，以及改善机械证明性能。你可以把一个证明命题想象成有一些输入条件。这些是证明语句上下文中可用的条件和标签。证明语句的输出是calc语句的第一行和最后一行的传递连接，无标记的assert或assert by语句中的条件，以及有标记的断言的标签。

# 参考文献

[0]Edsger W. Dijkstra and W. H. J. Feijen. A Method of Programming. Addison-Wesley, July 1988. 🔎 (opens new window)

[1]Leslie Lamport. How to write a 21st century proof. Technical report, Microsoft Research, 2011. https://lamport.azurewebsites.net/pubs/proof.pdf (opens new window). 🔎 (opens new window)

[2]K. Rustan M. Leino and Clément Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 361–381. Springer, 2016. 🔎 (opens new window)

[3]K. Rustan M. Leino and Nadia Polikarpova. Verified calculations. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments — 5th International Conference, VSTTE 2013, Revised Selected Papers, volume 8164 of Lecture Notes in Computer Science, pages 170–190. Springer, 2014. 🔎 (opens new window)

编辑 (opens new window)
上次更新: 2022/03/27, 00:29:25
各种推导式
集合元素上的函数

← 集合元素上的函数→

最近更新
01
寻找最大和最小数
04-06
02
斐波那契数列
04-06
03
线性查询
04-06
更多文章>
Theme by Vdoing | Copyright © 2022-2022 Li Jiahai | Dafny Community | 2022