formal-verification - 在 Dafny 中显示循环均匀性

Question

这是我要证明的代码:

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

但是我得到了一个后置条件错误:

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.

如果有任何方法可以证明均匀性的循环版本(while 循环或递归)，我将不胜感激!

编辑:从代码中可能不是很明显，但我正在寻找关于 n 的归纳证明，dafny 至少应该能够找出方法案例。

我看过一些类似的证明，其中递归函数用于方法函数的循环不变量，只是不知道为什么它不适用于这种特殊情况。

您可以在此处试用 rise4fun 上的代码: https://rise4fun.com/Dafny/wos9

Answer 1

我发现在证明您的实现后置条件时存在问题，如果您从零开始，您可以为 0 建立循环不变量并从那里开始。

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

最后一步需要一个引理来从最终的两种可能情况中为 i，(i==n) 或 (i==n+1) 建立否定情况。

希望对您有所帮助。