Dfenyは以下のように集約します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; 
    } 
} 

Answer 1

：

invariant forall idx :: idx in ret ==> idx % 2 == 0 

それはretアレイ内のすべてのメンバーが不変

invariant forall idx :: 0 <= idx < i ==> (idx in ret ==> idx % 2 == 0)

が失敗している2 で割り切れるであることを意味retには、状態がのメンバーが含まれている可能性があるため3210は真ですが、2で割り切れないかもしれません。このコードを考えてみましょう：http://www.rise4fun.com/Dafny/W7RwL