Dafny
lijiahai
2022-03-25

循环不变式

# 循环不变式

“while”循环给Dafny带来了一个问题。Dafny无法提前知道代码将循环多少次。但是Dafny需要考虑程序中的所有路径，这可能包括循环任意次数。为了使Dafny能够使用循环，您需要提供循环不变式，这是另一种注释。 循环不变式是在进入循环时以及每次循环体执行后保存的表达式。它捕获了一些不变的东西，也就是说，在循环的每一步中都是不变的。现在，很明显，我们需要在每次循环的时候改变变量，等等，否则我们就不需要循环了。像前置条件和后置条件一样，不变量是一个属性，它在每次循环执行时都被保留，使用我们已经看到的布尔表达式表示。例如，我们在上面的循环中看到，如果' i '一开始是正的，那么它就一直是正的。因此，我们可以使用它自己的关键字将不变量添加到循环中:

method m(n: nat)
{
   var i := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
}
   var i := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

当您指定一个不变量时，Dafny证明了两件事:不变量在进入循环时保持不变，并且被循环保存。通过保留，我们的意思是假设在循环开始时不变式保持不变，我们必须证明执行循环体一次使不变式再次保持不变。Dafny只能在分析循环体时知道不变量说了什么，除了循环保护(循环条件)。就像Dafny自己不会发现方法的属性一样，除非通过一个不变量告诉它，否则它只会知道循环的最基本属性被保留。 在我们的例子中，循环的重点是每次建立一个(好吧，两个)斐波那契数，直到我们达到想要的数。退出循环后，我们将得到' i == n '，因为当i达到' n '时，' i '将停止递增。我们可以使用断言技巧来检查Dafny是否也看到了这个事实:

method m(n: nat)
{
   var i: int := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
   assert i == n;
}
   var i: int := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
   assert i == n;
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

我们发现这个断言失败了。据Dafny所知，在循环过程中的某个点上，“i”可能以某种方式变得比“n”大得多。在循环退出后(即在循环结束后的代码中)，它所知道的是循环保护失败，不变量保持不变。在本例中，这相当于' n <= i '和' 0 <= i '。但这并不足以保证' i == n '，只保证' n <= i '。我们需要消除i超过n的可能性。解决这个问题的第一个猜想可能是:

method m(n: nat)
{
   var i: int := 0;
   while i < n
      invariant 0 <= i < n
   {
      i := i + 1;
   }
}
   var i := 0;
   while i < n
      invariant 0 <= i < n
   {
      i := i + 1;
   }
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

这并不验证，因为Dafny会报错循环没有保存(也称为没有维护)不变式。我们希望能够说，在循环结束后，所有不变式都保留下来。我们的不变式适用于循环的每一次执行，除了最后一次。因为循环体只有在循环保护生效时才执行，所以在最后一次迭代中，‘i’从‘n - 1’到‘n’，但在循环退出时不会进一步增加。因此，我们只从我们的不变量中省略了一种情况，修复它相对容易:

method m(n: nat)
{
   var i: int := 0;
   while i < n
      invariant 0 <= i <= n
   {
      i := i + 1;
   }
}
...
   invariant 0 <= i <= n
...
1
2
3
4
5
6
7
8
9
10
11
12

现在，我们可以说，‘n <= i’来自循环保护，‘0 <= i <= n’来自不变量，这允许Dafny证明‘i == n’断言。选择循环不变量的挑战在于找到一个被循环保留的不变量，而且它还能让您证明在循环执行后需要什么。

练习7. 将循环不变量改为' 0 <= i <= n+2 '。循环是否仍然验证?断言' i == n '在循环之后仍然验证吗?

method m(n: nat)
{
   var i: int := 0;
   while i < n
      invariant 0 <= i <= n  // Change this. What happens?
   {
      i := i + 1;
   }
   assert i == n;
}
   invariant 0 <= i <= n+2
1
2
3
4
5
6
7
8
9
10
11

练习8. 使用原来的循环不变式，将循环守卫从' i < n '更改为' i != n '。循环和循环后的断言仍然进行验证吗?为什么或为什么不?

method m(n: nat)
{
   var i: int := 0;
   while i < n  // Change this. What happens?
      invariant 0 <= i <= n
   {
      i := i + 1;
   }
   assert i == n;
}
   while i != n ...
1
2
3
4
5
6
7
8
9
10
11

除了计数器之外，我们的算法还需要一对表示序列中相邻斐波那契数列的数字。不出所料，我们将有另外一两个不变式来将这些数字和计数器联系起来。为了找到这些不变量，我们使用了一种常见的Dafny技巧:从后置条件向后计算。 斐波那契方法的后置条件是返回值' b '等于' fib(n) '。但是在循环之后，我们有了' i == n '，所以在循环的最后我们需要' b == fib(i) '。这可能是一个很好的不变量，因为它与循环计数器相关。这种现象在Dafny的程序中非常普遍。通常，一个方法只是一个循环，当它结束时，通过使计数器达到另一个数字，通常是一个参数或数组或序列的长度，使后置条件为真。变量b，也就是我们的输出参数，将会是当前的斐波那契数列:

   invariant b == fib(i)
1

我们还注意到，在我们的算法中，我们可以通过跟踪一对数字来计算任何斐波那契数，并将它们相加得到下一个数字。我们想要一种方法来追踪之前的斐波那契数，我们称之为' a '另一个不变式将表示该数字与循环计数器的关系。不变量有:

   invariant a == fib(i - 1)
1

在循环的每一步，对这两个值求和以得到下一个前导数，而后面的数字是旧的前导数。使用并行赋值，我们可以编写一个循环来执行以下操作:

function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}
method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
   var i := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
}
   var i := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
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

这里' a '是结尾数，' b '是前导数。并行赋值意味着在对变量赋值之前计算整个右手边。因此，“a”将得到“b”的旧值，而“b”将得到两个旧值的和，这正是我们想要的行为。 我们还对循环计数器' i '进行了更改。因为我们还想跟踪后面的数字，所以我们不能从0开始计数器，否则我们将不得不计算一个负的斐波那契数。这样做的问题是，当我们进入循环时，循环计数器不变式可能不成立。唯一的问题是当n为0时。这可以作为一种特殊情况消除，方法是在循环开始时测试该条件。完成的斐波那契方法变成:

function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}
method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
   if n == 0 { return 0; }
   var i: int := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
}
method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
   if n == 0 { return 0; }
   var i: int := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
}
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
35
36
37
38

Dafny不再报错循环不变式不成立，因为如果' n '为零，它将在到达循环之前返回。Dafny还能够使用循环不变量来证明，在循环之后，' i == n '和' b == fib(i) '，它们一起隐含了后置条件' b == fib(n) '。

练习9. 上面的' ComputeFib '方法比必要的要复杂得多。写一个简单的程序，不引入' a '作为' b '前面的斐波那契数，而是引入一个变量' c '在' b '后面。根据斐波那契数列的数学定义来验证你的程序是正确的。

function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}
method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)  // Do not change this postcondition
{
   // Change the method body to instead use c as described.
   // You will need to change both the initialization and the loop.
   if n == 0 { return 0; }
   var i: int := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
}
method ComputeFib(n: nat) returns (b: nat)
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

练习10. 从上面完成的' ComputeFib '方法开始，删除' if '语句，并将' i '初始化为' 0 '，' a '初始化为' 1 '，' b '初始化为' 0 '。通过调整循环不变量来匹配新的行为来验证这个新程序。

function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}
method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
   var i: int := 0;
   var a := 1;
       b := 0;
   while i < n
      // Fill in the invariants here.
   {
      a, b := b, a + b;
      i := i + 1;
   }
}
method ComputeFib(n: nat) returns (b: nat)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

使用不变量的一个问题是，很容易忘记让循环“取得进展”，即在每一步做工作。例如，我们可以在前面的程序中省略整个循环体。这些不变量是正确的，因为它们在进入循环时仍然为真，而且由于循环没有改变任何东西，它们将被循环保存下来。我们知道，如果退出循环，那么我们可以假设守卫和不变量为负值，但这并没有说明如果我们永远不退出循环会发生什么。因此，我们希望确保循环在某个点结束，这给了我们一个更强的正确性保证(技术术语是完全正确性)。

编辑 (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