终止

Dafny通过使用减注释证明了代码的终止，即不会永远循环。对于许多事情，Dafny能够猜出正确的注释，但有时需要明确说明。事实上，对于我们到目前为止看到的所有代码，Dafny都能够自己进行这种证明，这就是为什么我们还没有看到显式的减小注释。Dafny在两个地方证明了终止:循环和递归。这两种情况都需要Dafny明确的注释或正确的猜测。 减小注释，顾名思义，为Dafny提供了一个表达式，该表达式在每次循环迭代或递归调用时都会减小。在使用减小表达式时，Dafny需要验证两个条件:表达式实际上变得更小，以及它是有界的。很多时候，整数值(自然或普通整数)是减少的量，但也可以使用其他东西。(详见参考资料)在整数的情况下，假定边界为零。例如，下面是在循环中正确使用(当然是用它自己的关键字):

method m ()
{
   var i := 20;
   while 0 < i
      invariant 0 <= i
      decreases i
   {
      i := i - 1;
   }
}
   while 0 < i
      invariant 0 <= i
      decreases i
   {
      i := i - 1;
   }

这里Dafny拥有证明终止所需的所有条件。变量i在每次循环迭代中都会变小，并且小于0。这很好，除了循环是向后的大多数循环，这往往是向上而不是向下计数。在这种情况下，减少的不是计数器本身，而是计数器与上界之间的距离。下面是一个处理这种情况的简单技巧:

method m()
{
   var i, n := 0, 20;
   while i < n
      invariant 0 <= i <= n
      decreases n - i
   {
      i := i + 1;
   }
}
   while i < n
      invariant 0 <= i <= n
      decreases n - i
   {
      i := i + 1;
   }

这实际上是Dafny对这种情况的猜测，因为它看到i < n，并假设n - i是减少的数量。循环不变量的上界意味着0 <= n - i，并给了Dafny一个数量的下界。当n的边界不是常量时，这也适用，例如在二分搜索算法中，两个量彼此接近，且都不是固定的。

练习11.

点击查看题目

在上面的循环中，不变量i <= n和循环保护的否定允许我们在循环结束后结束i == n(正如我们之前用assert检查过的那样)。请注意，如果循环守卫被写成i != n(如练习8中所示)，那么无论循环不变量是什么，守卫的否定都会在循环之后立即给出i == n。将循环守卫更改为i != n，并删除不变注释。程序验证了吗?发生了什么事?

method m()
{
   var i, n := 0, 20;
   while i != n
      decreases n - i
   {
      i := i + 1;
   }
}
   while i != n

另一种需要终止证明的情况是递归方法或函数。与无限循环类似，这些方法可能永远调用自己，永远不会返回到它们的原始调用者。当Dafny无法猜出终止条件时，可以给出显式的减小子句以及前置和后置条件，就像对fib函数的不必要注释一样:

function fib(n: nat): nat
   decreases n
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}
function fib(n: nat): nat
   decreases n
{
   ...
}

与前面一样，Dafny可以自己猜测这个条件，但有时递减条件隐藏在对象的某个字段中或其他Dafny自己无法找到的地方，它需要一个显式注释。