Dafny收集下面的平均數N

Question

下面是一個整數爲lim的例子，它返回一個嚴格小於lim的整數序列，它們是偶數。

只有第二個不變量中的... <==> ...的向後方向不驗證。我嘗試過玩這個遊戲一段時間，但我一直無法弄清楚。

任何幫助非常感謝！

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

您需要添加這個不變的：由2 的不變

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

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

這意味着ret陣列中的所有成員都整除失敗因爲ret可能包含條件爲的成員3210是真實的，但它們可能不能被2整除。請考慮以下代碼：http://www.rise4fun.com/Dafny/W7RwL