formal-verification - Dafny は N 以下の偶数を収集します

Question

limこれは、整数を取り、それより厳密に小さいlim偶数のすべての整数のシーケンスを返す例です。

2 番目の不変量の逆方向のみが... <==> ...検証されません。私はしばらくこれをいじってみましたが、理解できませんでした。

どんな助けでも大歓迎です！

method evens(lim : int) returns (ret : seq<int>)
  requires 0 < lim
{
  ret := [];

  var i := 0;

  while (i < lim)
    invariant 0 <= i <= lim
    invariant forall idx :: 0 <= idx < i ==> (idx % 2 == 0 <==> idx in ret)
  {
    if (i % 2 == 0) {
      ret := [i] + ret;
    }

    i := i + 1;
  }
}