即使不变断言有效，Dafny 循环不变性也会失败这是一个小错误吗？

问题描述

嗨，教学我正在设置大量简单的愚蠢问题。大部分情况下都很好，但是...要么我错过了有关 Dafny 中循环不变量的一些细节，要么这是一个弱点/错误？

method whS(a:int) returns ()
  {   var i:int := 0;
       while (i<a ) 
       decreases a-i     
       invariant i<= a
       {   assert i<= a;
            i:=i+1;
           assert i<= a;
       }  
   }  

该方法无法验证，并出现错误“invariant may not hold on entry”然而，在注释掉不变量的情况下，该方法即使使用断言也能验证。

解决方法

记住“循环不变量何时必须为真？”这个问题的答案的好方法。在 Dafny 中是“每当循环条件被评估时”。

所以循环不变量需要在循环的第一次迭代之前为真，即使主体永远不会执行，因为循环条件将被评估以确定是否完全进入循环.不变量也需要在最后一次迭代之后为真，因为将再次评估循环条件以确定是否执行另一次迭代。

在您的示例中，如果方法的参数 a 为负，则循环不变量在第一次评估循环条件之前为假。一个适用于此循环的不变量的示例类似于 a >= 0 ==> i <= a。

,

非常感谢詹姆斯 我可以看到我误解了 dafny 如何实现循环不变量。将 while 包装在 if 语句中现在可以验证并为我提供我自己认为的语义。

method whS(a:int) returns ()
  {   var i:int := 0;
       if (i<a) {
         while (i<a ) 
           decreases a-i     
           invariant i<= a 
          {  i:=i+1;
          }  
       }
   }

再次感谢詹姆斯。我在星期二讲课时会避免这个错误。