CODEWITHSUNDEEP
formal-verificationdafny
rausted
rausted

Reputation: 959

Show loopy eveness in Dafny

This is the code I’m trying to prove:

function rec_even(a: nat) : bool
  requires a >= 0;
{
   if a == 0 then true else
   if a == 1 then false else
                  rec_even(a - 2)
}


method Even(key: int) returns (res: bool)
  requires key >= 0;
  ensures res == rec_even(key)
{   
  var i : int := key;
  while (i > 1)
    invariant  0 <= i <= key;
    decreases i;
  {
    i:= i - 2;
  }
  res := i == 0;
}

But I’m getting a postcondition error:

stdin.dfy(13,0): Error BP5003: A postcondition might not hold on this return path. stdin.dfy(12,14): Related location: This is the postcondition that might not hold.

If there’s any way to prove a loopy version of the evenness (while loop or recursive) I would be grateful!

EDIT: It might not be obvious from the code, but I'm looking for an inductive proof on n which dafny should be able to figure out at least for the method case.

I've seen some similar proofs where the recursive function is used in the loop invariant of the method function, just don't know why it doesn't work for this particular case.

You can try the code on rise4fun here: https://rise4fun.com/Dafny/wos9

Upvotes: 3

Views: 272

Answers (1)

Joao Costa Seco
Joao Costa Seco

Reputation: 46

I see a problem with proving the post-condition your implementation, if you start from zero, you may establish the loop invariant for 0 and go from there.

function rec_even(a: nat) : bool
    decreases a
{
    if a == 0 then true else
    if a == 1 then false else
    rec_even(a - 2)
}

lemma {:induction a} Lemma(a:int)
    requires 1 <= a
    ensures rec_even(a-1) ==> !rec_even(a)
    {

    }

method Even(n: int) returns (res: bool)
requires n >= 0;
ensures res == rec_even(n)
{   
    var i : int := 0;
    while (i < n)
        invariant  0 <= i <= n+1;
        invariant rec_even(i)
        decreases n-i;
    {
        i:= i + 2;
    }
    assert rec_even(i);
    Lemma(i+1);
    assert i == n ==> rec_even(n);
    assert i == n+1 ==> !rec_even(i+1);
    res := i == n;
}

The last step needs a lemma to establish the negative case from the two possible cases in the end for i, (i==n) or (i==n+1).

Hope it helps.

Upvotes: 3

Related Questions