终止

Dafny证明所有程序终止。有两个潜在的非终止(发散)行为来源:循环，递归函数和方法。Dafny使用一种技术来处理这两种情况，减少注释。

递减注释指定一个称为终止度量的值，该值在每次遍历循环或每次调用递归函数或方法时严格变小。这个值也是有界的，因此它不会永远减小。这样，如果值从任意有限值开始，循环或递归必须停止。为了证明这一点，Dafny证明了终止度量在每次迭代中变得更小。如果Dafny无法证明这一点，它表示没有减少终止措施。因为每一种终止措施都有一个内置的下界，这就是Dafny需要做的，以证明终止。

Dafny可以在递减注释中使用几种类型的值，但最常见的是整数。整数有一个自然的下界，0，而且通常很容易证明它们是递减的。由于许多循环遍历索引，这类终止证明非常常见。例如，我们可能有以下循环:

method m(n: nat)
{
   var i := 0;
   while i < n
      invariant 0 <= i <= n
   {
      // do something interesting
      i := i + 1;
   }
}

while i < n
   invariant 0 <= i <= n
{
   // do something interesting
   i := i + 1;
}

如果我们把这个交给Dafny，就能立即证实。但是它是怎么知道它会终止的呢?因为这是如此常见的循环形式，Dafny有一个猜测终止度量的特殊规则。Dafny看到没有显式的递减注释，所以它尝试猜测一个。它看到循环条件是A < B形式的比较，对于某些A和B，所以它做出猜测:

  decreases B - A

如果这样的话

  decreases n - i

如果我们将这个注释添加到循环中，它将继续进行验证。Dafny实际上没有那么严格要求终止测度为0。它真正需要的是，当终止度量为负时，循环不会再次执行。所以我们可以这样写:

method m()
{
   var i, n := 0, 11;
   while i < n
      decreases n - i
   {
      // do something interesting
      i := i + 5;
   }
}

var i, n := 0, 11;
while i < n
   decreases n - i
{
   // do something interesting
   i := i + 5;
}

这里，在最后一次迭代中，i变成了15，所以终止测度是-4。但在这里，循环保护为假，所以循环不会再次执行。注意，我们必须删除循环不变式，因为i现在可以超过n。

Dafny证明了整个程序的终止，而不仅仅是循环。为此，它对递归函数和方法使用了相同的技术。Dafny分析哪些函数/方法彼此调用，以找出可能的递归。对于每个可能递归的函数/方法，它需要显式或隐式减少函数或方法上的注释。大多数递归函数/方法都是自递归的: Dafny证明了整个程序的终止，而不仅仅是循环。为此，它对递归函数和方法使用了相同的技术。Dafny分析哪些函数/方法彼此调用，以找出可能的递归。对于每个可能递归的函数/方法，它需要显式或隐式减少函数或方法上的注释。大多数递归函数/方法都是自递归的:

function fac(n: nat): nat
{
   if n == 0 then 1 else n * fac(n-1)

Dafny接受了这个计划。对于大多数递归函数来说，它们只是用更小的参数值来调用自己，所以参数减少是默认的猜测。可以通过添加以下内容:

decreases n

到函数声明来明确decreases注释

有时，具有可能不会终止的循环或终止证明未知的循环是有益的。例如，考虑以下方法:

method hail(N: nat)
   decreases *
{
   var n := N;
   while 1 < n
      decreases *
   {
      n := if n % 2 == 0 then n / 2 else n * 3 + 1;
   }
}

这个程序终止当且仅当Collatz猜想为真时，这是一个数学上的开放问题，所以你不能期望Dafny能够证明终止。您还可以编写流处理器之类的代码，以便永远运行。因此，Dafny提供了一个“out”，一个特殊的注释，指示Dafny不要试图证明终止，这在前面的hail方法中已经给出。这可以用于所有非鬼循环。注意，如果一个方法包含一个标记为decreases *的循环，那么它本身也必须被标记为decreases *。

Dafny可以使用整数以外的值作为终止度量。当指定序列时，Dafny自动使用长度作为终止度量。如果一个集合是另一个集合的严格子集，则认为这个集合更小，因此每个集合必须包含在前面的集合中。对于集合，空集合是尽可能小的，序列有自然数长度，所以这两个都有下界。虽然不是非常有用，但也可以在递减子句中使用bool和references。(如果你想了解细节，请参阅参考资料。)最后的终止度量是其他类型度量的元组。例如，下面的Ackermann函数的实现使用一对整数来证明终止

function Ack(m: nat, n: nat): nat
   decreases m, n
{
   if m == 0 then n + 1
   else if n == 0 then Ack(m - 1, 1)
   else Ack(m - 1, Ack(m, n - 1))
}

在这里，递减子句被明确地写了出来，尽管Dafny会猜出完全相同的事情。元组使用组件值的大小比较来确定度量值是否缩水。在这种情况下，它使用两个整数，但一般来说，不同的部分可以属于不同的类别。这种比较是按词典编纂的。如果第一个元素，在这里是m，比其他的值小没关系。它们可以增加，减少，或保持不变。只有当第一个元素不变时，才考虑第二个元素。然后，第二个值需要减小。如果没有，则第三个元素必须减少，以此类推。最终，必有一种元素会减少。过了这个点，其他元素就可以自由增加或做它们想做的事。 在Ack函数中，有三个递归调用。在第一种情况下，m变小1，但n增大。这很好，因为在元组中n在m后面。在第二个调用中，m也减少了，因此第二个参数允许是任何值(这很好，因为Dafny实际上并没有证明关于第三个递归调用的结果的任何东西)。Dafny确实需要证明第三通电话符合终止措施。对于这个调用，m保持不变，但n减小，因此总体度量也减小了。 终止不仅适用于单个函数/方法，还适用于多个相互递归的函数/方法。例如，考虑这对递归定义的奇偶校验谓词:

predicate even(n: nat)
   ensures even(n) <==> n % 2 == 0
{
   if n == 0 then true else odd(n-1)
}
predicate odd(n: nat)
   ensures odd(n) <==> n % 2 != 0
{
   if n == 0 then false else even(n-1)
}

Dafny通过考虑两个函数中所有可能的路径证明了它们的终止。