dafny - Dafny: 両方の量指定子を一緒に使用する方法

Question

Dafny を使用して、非常に単純なコードを検証しようとしています。拳ブロックは通常版。そして、事後条件を設定する方法が見つかりません

「私はすべてのjのために存在します~~~~~~」

Dafny で 2 つの量指定子を一緒に使用する方法がわかりません。助けてください。ありがとう。

//this is a c++ version of the code
for (int lastNot0 = 0, cur = 0; cur < nums.length; cur++) {
    if (nums[cur] != 0) {
        swap(nums[lastNot0 ++], nums[cur]);
    }
}

//Dafny code
method moveZero(a: array<int>)
  requires a != null && a.Length > 0;
  modifies a;
  ensures exists i :: forall j :: 0 <= j < i < a.Length && a[j] != 0;
//  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var lastNot0 := 0;
  var cur := 0;
  while(cur < a.Length)
  invariant 0 <= lastNot0 <= cur < a.Length
  {
    if(a[cur] != 0){
      swap(a, lastNot0, cur);
      lastNot0 := lastNot0 + 1;
    }
    cur := cur + 1;

  }
}

method swap(a: array<int>, i: int, j: int)
  requires a != null && 0 <= i < j < a.Length;
  modifies a;
  ensures a[i] == old(a[j]);
  ensures a[j] == old(a[i]);
  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var temp := a[i];
  a[i] := a[j];
  a[j] := temp;
}