Dafny, post condition does not hold after loop

Question

In the following method, Dafny reports that the postcondition might not hold, even though I am quite sure that it does.

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

Indeed, the postcondition does always hold, but Dafny cannot tell!

That's because you're missing a loop invariant annotation such as

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

After adding that line to the loop, the method verifies.

For more explanation about why Dafny sometimes reports errors on correct programs, see the (brand new) FAQ. For more about loop invariants, see the corresponding section in the rise4fun guide.