dafny - ソートされた事後条件が成り立たない

Question

メソッドでやりたいことは、前の配列を上書きして、並べ替えられた数値で埋めることですが、dafny は、事後条件が保持されず、私の人生では理由を理解できないと言っています。ループに不変条件を追加する必要があると思いますが、ループに入る前にチェックされるため、有効な不変条件を配置する方法がわかりません。

method sort2(a : array<int>)
modifies a;
requires a != null && a.Length >= 2;
ensures sorted2(a[..]);
{
  var i := a.Length - 1;
  while (i >= 0)
  decreases i
 {
     a[i] := i;
     i := i - 1;
 }
}

predicate sorted2(s: seq<int>)
{
    forall i :: 1 <= i < |s| ==> s[i] >= s[i-1]
}

私の以前の試みは a を再初期化することだけでしたが、dafny はメソッド内でそれを許可していないようです。