dafny初始断言在循环中不验证，但最终断言验证

如何解决dafny初始断言在循环中不验证，但最终断言验证

嗨，我已将问题简化为只将一个数组的元素复制到另一个数组的方法。我的问题是，即使我有保护措施确保初始断言仅在第一次进入循环后才适用，但最终断言仍会验证，而初始断言仍无法验证。因此，我认为最终断言应该暗示初始断言。

非常感谢任何帮助。

method simpImp(a:array<int>) returns (r:array<int>)
   {
    print "a ",a[..],"\n";
    r := new int[a.Length];  
    var i:nat := 0;
    while (i< a.Length) 
      decreases a.Length - i
      invariant a.Length  >= i
    {
        if (i> 0) { print  "  bool  ",r[i-1] == a[i-1],"\n";}
        else {print "*i ",i,"\n";}
        //if (i> 0) { assert   r[i-1] == a[i-1]; } //Fail
        //assert  (i>0) ==> r[i-1] == a[i-1];      //Fail
         r[i] := a[i];  
         i:= i +1;
        assert    r[i-1] == a[i-1]; 
    }
  }
method Main() {
var a:array<int> := new int[5];
a[0],a[1],a[2],a[3],a[4] := 10,2,30,4,3;
var iny:= simpImp(a);
print "r ",iny[..],"\n";
}

解决方法

问题是您需要在循环不变式中添加一些内容以“记住”两次迭代之间需要携带的所有事实。 Dafny仅在循环体的开头假设循环不变式，然后单独分析循环体。因此，除非您将事实添加到循环不变式中，否则Dafny将其“遗忘”。

在您的简化示例中，添加

    invariant i > 0 ==> r[i-1] == a[i-1]

进入循环会导致程序进行验证。

---

您可以在this answer的后半部分了解有关循环不变式的更多信息。请注意，讨论的用语是建立保留循环不变式的意思，但是其推理与尝试确定循环主体内部的断言有效是完全相同的。请随时提出其他问题！