Dafny собирает evens ниже 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

Вам нужно добавить этот инвариант:

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

Это подразумевает, что все члены в ret массиве делится на 2. Инвариантная

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

не удается т.к. ret может содержать участников, у которых есть условие 0 <= idx < i верно, но они могут не делиться на 2. Рассмотрим этот код: http://www.rise4fun.com/Dafny/W7RwL