arrays - Dafny Insert int into Sorted Array メソッド

Question

このプログラムを dafny で証明しようとしていますが、最後の不変条件でエラーが発生し、なぜ機能しないのかわかりません。

このプログラムは、ソートされた配列に int を挿入するメソッドで構成されています。int は正しい位置に挿入されます。つまり、5 を 1,2,3,4,5,6,7 に挿入すると、次の値が返されます: 1,2,3,4,5,5,6,7

function sorted (a: array<int>): bool
  requires a != null ;
  reads a;
  {
    forall i :: 0 <= i < (a.Length - 1) ==> a[i] <= a[ i+1]
  }

method InsertSorted(a: array<int>, key: int ) returns (b: array<int>)
  requires a != null && sorted(a);
  ensures b != null ;
  ensures sorted(b);
   {
     var i:= 0;
     b:= new int[a.Length + 1];

     if(a.Length > 0){
      while (i < a.Length)
      invariant 0<= i;
      invariant i <= a.Length;
      invariant b.Length == a.Length + 1;
      invariant sorted(a);
      invariant forall j :: 0 <= j < i ==> b[j] <= b[j+1];
      {
        if(a[i]<=key)
        {
          b[i]:= a[i];
          b [i+1] := key;
          assert b[i] <= b[i+1];         
        }
        else if (key > a[i])
        {
          if(i==0)
          {
            b[i] := key;
          }
          b [i+1] := a[i];
          assert key > a[i];
          assert b[i]<= b[i+1];
        }
        else{
          b[i]:= a[i];
          b [i+1] := a[i];
          assert sorted(a);
          assert b[i] <= b[i+1];
        }
        assert b[i]<= b[i+1];
        i := i+1;
      }
     }
     else{
       b[0] := key;
     }
   }

ありがとう