如何证明包含return语句的Dafny循环程序？

要让Dafny验证通过这个程序的后置条件r == 5，核心是补充更精确的循环不变式，给验证器提供足够的逻辑线索来跟踪循环行为。

问题根源 #

原循环不变式0<= i <=10过于宽泛，无法体现关键逻辑：只要循环还在执行，说明i还没到过5（否则已经触发提前返回）。验证器无法仅凭这个弱不变式推断出“所有返回路径都返回5”。

修正方案：增强循环不变式 #

我们需要添加一个不变式，明确“当前i之前的所有取值都不等于5”，让验证器能推断出：当i增长到5时一定会触发return，且循环永远不会执行到i>=6的情况。

修正后的完整代码：

method return_loop() returns (r:int)
ensures r == 5
{
  var i := 0;
  while i < 10
    invariant 0<= i <= 10
    invariant forall k: int :: 0 <= k < i ==> k != 5
  {
    if i == 5{
       return i;
    }
    i := i + 1;
  }
  return i;
 }

验证逻辑说明 #

1. 初始状态：i=0，第二个不变式的范围0<=k<0是空集，自动满足，不变式成立。
2. 循环迭代：
   • 若i !=5，根据第二个不变式可推导出i<5（否则k=5会落在0<=k<i范围内，与k!=5矛盾），因此i++后i<=5，且新的i仍满足“之前所有取值都不等于5”。
   • 当i=5时，进入循环体触发return i，直接满足后置条件r==5。
3. 循环终止分支：若循环因i>=10终止，意味着k=5落在0<=k<i范围内，与第二个不变式矛盾，因此这个分支永远不会执行。

通过上述不变式，Dafny可以完整证明程序的正确性。

内容的提问来源于stack exchange，提问作者Anwar