在 Dafny 中显示循环均匀度答案

【问题标题】：Show loopy eveness in Dafny在 Dafny 中显示循环均匀度
【发布时间】：2018-08-26 04:34:52
【问题描述】：

这是我要证明的代码：

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

【问题讨论】：

添加了一个rise4fun链接，希望能更容易获得帮助

标签： formal-verification dafny

【解决方案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)。

希望对您有所帮助。

【讨论】：