Dafny
lijiahai
2022-03-25
目录

断言

# 断言

与前置条件和后置条件不同，断言被放置在方法的中间。像前面两个注释一样，断言有一个关键字assert，后面跟着布尔表达式和结束简单语句的分号。断言表示，当控制到达代码的这一部分时，特定的表达式总是保持不变。例如，下面是一个在虚拟方法中使用断言的简单例子:

method Testing()
{
   assert 2 < 3;
   // Try "asserting" something that is not true.
   // What does Dafny output?
}
method Testing()
{
   assert 2 < 3;
}
1
2
3
4
5
6
7
8
9
10

Dafny证明了这种方法是正确的，因为2总是小于3。断言有几个用途，但其中最主要的是检查你的期望在不同的点上是否真的是真的。如上所述，您可以使用它来检查基本的算术事实，但它们也可以用于更复杂的情况。通过检查Dafny能够证明您的代码，断言是调试注释的强大工具。例如，我们可以用它来研究Dafny对Abs函数的了解。 为此，我们还需要一个概念:局部变量。局部变量的行为与您所期望的完全一样，除了可能存在一些与遮蔽有关的问题。(详见参考资料)局部变量用var关键字声明，并且可以有类型声明。与需要类型的方法参数不同，Dafny几乎可以在所有情况下推断出局部变量的类型。下面是一个初始化的显式类型变量声明的例子:

method m()
{
   var x: int := 5;
}
   var x: int := 5;
1
2
3
4
5

在这种情况下，可以删除类型注释:

method m()
{
   var x := 5;
}
   var x := 5;
1
2
3
4
5

可以同时声明多个变量:

method m()
{
   var x, y, z: bool := 1, 2, true;
}
   var x, y, z: bool := 1, 2, true;
1
2
3
4
5

显式类型声明只适用于紧接在前面的变量，因此这里的bool声明只适用于z，而不适用于x或y，它们都被推断为int。我们需要变量，因为我们想讨论Abs方法的返回值。我们不能直接将Abs放入规范中，因为该方法可能会改变内存状态以及其他问题。因此，我们捕获调用Abs的返回值如下:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
}
// use definition of Abs() from before.
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

这是一个例子，我们可以问Dafny它知道代码中的值，在这个例子中是v。我们通过添加断言来实现，就像上面的断言一样。每当Dafny遇到断言时，它都会试图证明该条件适用于代码的所有执行。在本例中，通过该方法只有一条控制路径，Dafny能够轻松地证明注释，因为它正是Abs方法的后向条件。Abs保证返回值是非负的，所以它很容易跟随v，也就是这个值，在调用Abs之后是非负的。

练习1

点击查看题目及代码

编写一个测试方法，调用练习0中的Max方法，然后对结果进行断言处理。

method Max(a: int, b:int) returns (c: int)
  // Use your code from Exercise 0
method Testing() {
  // Assert some things about Max. Does it operate as you expect?
  // If it does not, can you think of a way to fix it?
}
method Testing() { ... }
1
2
3
4
5
6
7

但我们对Abs法有更深的了解。特别是对于非负的x，Abs(x) == x。具体来说，在上面的程序中，v的值为3。如果我们尝试添加一个断言(或更改现有的断言):

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
   assert v == 3;
}
   assert v == 3;
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

我们发现Dafny不能证明我们的断言，并给出一个错误。发生这种情况的原因是，Dafny忘记了除当前正在处理的方法之外的所有方法的主体。这极大地简化了Dafny的工作，也是它能够以合理速度运行的原因之一。它还通过将程序分解来帮助我们对程序进行推理，这样我们就可以单独分析每个方法*(给出其他方法的注释)*。当我们调用每个方法时，我们根本不关心它内部发生了什么，只要它满足它的注解。这是可行的，因为Dafny将证明所有的方法都满足它们的注释，并拒绝编译我们的代码，直到它们满足。

对于Abs方法，这意味着Dafny在test方法中所知道的关于Abs返回值的唯一信息就是后置条件对它的说明，仅此而已。这意味着Dafny不知道关于Abs和非负整数的好属性，除非我们把它放在Abs方法的后置条件中。另一种方法是将方法注释(以及参数和返回值的类型)视为修复方法行为的方法。在任何使用该方法的地方，我们假定它是满足前置和后置条件的任何一种可想象的方法。在Abs情况下，我们可以这样写:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   y := 0;
}
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
   // this stil does not verify, but now it is actually not true:
   assert v == 3;
}
method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   y := 0;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

该方法满足后置条件，但显然满足程序片段:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   y := 0;
}
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
   assert v == 3;
}
   var v := Abs(3);
   assert v == 3;
1
2
3
4
5
6
7
8
9
10
11
12
13

在这个例子中是不成立的。Dafny正在以一种抽象的方式考虑带有这些注释的所有方法。数学绝对值当然是这样一种方法，但是所有返回正常数的方法也是这样。我们需要更强的后置条件来消除这些其他可能性，并将方法修正为我们想要的方法。我们可以通过以下方法部分地做到这一点:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> y == x
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> y == x
{
   // body as before
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

这正好表达了我们之前讨论过的性质，即非负整数的绝对值是相同的。第二个确保是通过隐含操作符表示的，它基本上说，在数学意义上，左边意味着右边(它的绑定比布尔and和比较更弱，所以上面说，0 <= x意味着y == x)。左右两边必须都是布尔表达式。 后置条件是，在Abs被调用后，如果x的值是非负的，那么y等于x。这个暗示的一个警告是，如果左部分(先行词)为假，它仍然为真。所以当x为负时第二个后置条件是成立的。事实上，注解说的唯一一件事是当x为负时，结果y为正。但这仍然不足以修复该方法，所以我们必须添加另一个后置条件，以使以下完整的注释覆盖所有情况:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> y == x
   ensures x < 0 ==> y == -x
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> y == x
   ensures x < 0 ==> y == -x
{
   // body as before
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

这些注释足以要求我们的方法实际计算x的绝对值。这些后置条件并不是表示该属性的唯一方法。例如，这是表达同一件事的一种不同的，稍微简短的方式:

method Abs(x: int) returns (y: int)
   ensures 0 <= y && (y == x || y == -x)
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
   ensures 0 <= y && (y == x || y == -x)
1
2
3
4
5
6
7
8
9
10

一般来说，有很多方法可以写出一个给定的性质。大多数时候，选择哪一个并不重要，但是一个好的选择可以使您更容易理解所述的属性并验证其正确性。 但我们仍然有一个问题:似乎有很多重复。方法的主体在注释中得到了非常密切的反映。虽然这是正确的代码，但我们希望消除这种冗余。正如您可能猜到的，Dafny提供了一种实现这一点的方法:函数。

练习2

点击查看题目及代码

使用前置条件，改变Abs，说它只能调用负值。将Abs的主体简化为一个返回语句，并确保该方法仍然被验证。

method Abs(x: int) returns (y: int)
   // Add a precondition here.
   ensures 0 <= y
   ensures 0 <= x ==> y == x
   ensures x < 0 ==> y == -x
{
   // Simplify the body to just one return statement
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Abs(x: int) returns (y: int) { ... }
1
2
3
4
5
6
7
8
9
10
11
12
13
14

练习3

点击查看题目及代码

保持Abs的后置条件与上面相同，将Abs的主体更改为y:= x + 2。为了进行验证，您需要使用什么前提条件来注释方法?如果主体是y:= x + 1，你需要什么前提条件?当你可以调用这个方法时，先决条件说了什么?

method Abs(x: int) returns (y: int)
   // Add a precondition here so that the method verifies.
   // Don't change the postconditions.
   ensures 0 <= y
   ensures 0 <= x ==> y == x
   ensures x < 0 ==> y == -x
{
  y:= x + 2;
}
method Abs2(x: int) returns (y: int)
   // Add a precondition here so that the method verifies.
   // Don't change the postconditions.
   ensures 0 <= y
   ensures 0 <= x ==> y == x
   ensures x < 0 ==> y == -x
{
  y:= x + 1;
}
method Abs(x: int) returns (y: int) { ... }
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#

编辑 (opens new window)
上次更新: 2022/03/26, 19:35:15
前置和后置条件
函数

← 函数→

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