使用后置条件修改 Dafny 中的数组

Question

尝试实现一个相当简单的方法，在其中传递一个空数组并将值放入其中（自然数）。

代码运行良好，但一个应该在我脑海中传递的简单后置条件却给我带来了错误。

method Main() {
  var a := new int[5];
  initialise(a);

}

method initialise(a: array<int>) 
modifies a
requires a.Length > 0
ensures forall i :: 0 <= i < a.Length ==> a[i] == i
{
    var i := 0;
    while i < a.Length
    invariant 0 <= i <= a.Length
    decreases  a.Length - i
  {
        a[i] := i;
        i := i + 1;
    }
}

错误：

A postcondition might not hold on this return path. Related location 1: Line: 10, Col: 8

Answer 1

你需要告诉 Dafny 循环维护的不变量。

添加后

invariant forall j :: 0 <= j < i ==> a[j] == j

证明通过了。