3

这是我要证明的代码：

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)：错误 BP5003：后置条件可能不会在此返回路径上成立。stdin.dfy(12,14)：相关位置：这是可能不成立的后置条件。

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

编辑：从代码中可能并不明显，但我正在寻找关于 n 的归纳证明，至少对于方法案例，dafny 应该能够弄清楚。

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

你可以在这里尝试rise4fun上的代码： https ://rise4fun.com/Dafny/wos9

4

1 回答 1

3

我发现证明你的实现的后置条件存在问题，如果你从零开始，你可以为 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)。

希望能帮助到你。

于 2018-03-20T15:17:04.547 回答