了解循环不变式和断言如何在dafny中工作

问题描述

我试图理解为什么我下面的断言失败了。我能理解这是因为循环不变，但是为什么Dafny会这样做呢？当我明确指出循环条件为i

method T ()
{
  var n := 10;
  var i := 0;
  while i < n
     invariant 0 <= i <= n + 2
  {
     i := i + 1;
  }
  
  assert i == n;
}

解决方法

要弄清楚循环结束时的真实情况，Dafny依赖两件事。一个是循环不变式，它将假定为真，另一个是循环防护（在您的情况下为i < n），它将假定为假。

因此，在循环之后，您可以立即断言0 <=i <= n+1 && !(i < n)，这意味着n <= i <= n+2。如果您将断言更改为

assert n <= i <= n+2 ;

这将验证。

现在，如果您将不变式增强为

invariant 0 <= i <= n

然后您可以在结尾处增强断言

 assert n <= i <= n ;

或更简单地

assert i == n ;

Dafny能够推断出一些您没有告诉它的循环不变式。在这种情况下，它将注意到循环未更改n。本质上，它将添加n==10作为额外的循环不变式。因此，如果按照我的建议更改不变式，则可以在末尾声明i==10。但是它仍然仅依赖于警卫是错误的，而循环不变式（您告诉它的和它自己推断出的那些）都是真实的。

对于您发布的循环，Dafny无法推断i <= n是循环不变式，即使您可能完全清楚这是不变式。

如果Dafny从后置条件向后工作以得出可能作为循环不变式尝试的东西，那将很有趣。例如。它可能会查看i==n和i<n并得出结论，它将需要作为循环不变的i<n || i==n（或更强的东西）并尝试一下。但这还不是Dafny要做的事情。