CODEWITHSUNDEEP
formal-verificationdafny
Ian Sweet
Ian Sweet

Reputation: 11

Dafny collect evens below N

Here's an example which takes an integer lim and returns a sequence of all integers strictly less than lim which are even.

Only the backward direction of the ... <==> ... in the second invariant does not verify. I have tried playing around with this for a while and I haven't been able to figure it out.

Any help is much appreciated! 

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;
  }
}

Upvotes: 1

Views: 187

Answers (1)

deLta
deLta

Reputation: 581

You need to add this invariant:

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

It implies that all the members in the ret array are divisible by 2. The invariant

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

is failing because ret might contain members for whom the condition 0 <= idx < i is true but they might not be divisible by 2. Consider this code: http://www.rise4fun.com/Dafny/W7RwL

Upvotes: 1

Related Questions