Dafny，后置条件在循环后不成立

Question

在以下方法中，Dafny 报告后置条件可能不成立，尽管我很确定它确实成立。

method toArrayConvert(s:seq<int>) returns (a:array<int>)
    requires |s| > 0
    ensures |s| == a.Length
    ensures forall i :: 0 <= i < a.Length ==> s[i] == a[i]  // This is the postcondition that might not hold.
{
    a := new int[|s|];
    var i:int := 0;
    while i < |s|
        decreases |s| - i
        invariant 0 <= i <= |s|
    {
        a[i] := s[i];
        i := i + 1;
    }

    return a;  // A postcondition might not hold on this return path.
}

Answer 1

确实，后置条件总是成立，但 Dafny 无法判断！

那是因为您缺少循环不变注释，例如

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

将该行添加到循环后，该方法进行验证。

有关为什么 Dafny 有时会在正确的程序上报告错误的更多解释，请参阅（全新）FAQ。有关循环不变量的更多信息，请参阅rise4fun guide 中的相应部分。