dafny - 一連の整数の要素の合計: ループ不変式はループによって維持されない可能性があります

Question

「Dafny 入門: ガイド」を読んだ後、最初のプログラムを作成することにしました。整数のシーケンスが与えられたら、その要素の合計を計算します。しかし、Dafny にプログラムを検証してもらうのに苦労しています。

function G(a: seq<int>): int
  decreases |a|
{
  if |a| == 0 then 0 else a[0] + G(a[1..])
}

method sum(a: seq<int>) returns (r: int)
  ensures r == G(a)
{
  r := 0;
  var i: int := 0;
  while i < |a|
    invariant 0 <= i <= |a|
    invariant r == G(a[0..i])
  {
    r := r + a[i];
    i := i + 1;
  }
}

私は得る

stdin.dfy(12,2): Error BP5003: A postcondition might not hold on this return path.
stdin.dfy(8,12): Related location: This is the postcondition that might not hold.
stdin.dfy(14,16): Error BP5005: This loop invariant might not be maintained by the loop.

プログラムを検証するために、Dafny には何らかの「助け」が必要なのではないかと思います (レンマかな?) が、どこから始めればよいかわかりません。