在Dafny中证明循环偶数性时遭遇后置条件错误求助

你的问题核心在于循环不变式不足以让Dafny推导出后置条件。原不变式只约束了i的取值范围，但没有建立起key和当前i在奇偶性上的等价关系——而这正是连接循环结束结果和递归函数rec_even的关键。

问题分析 #

递归函数rec_even的定义本质是：一个数是偶数，当且仅当它减2后依然是偶数（或等于0）。你的循环通过不断减2来缩小i，但Dafny不知道key和i始终保持相同的奇偶性，也就无法证明res == rec_even(key)。

修改后的代码 #

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;
    // 新增关键不变式：key和i的奇偶性等价，即rec_even结果一致
    invariant rec_even(key) == rec_even(i);
    decreases i; 
  { 
    i := i - 2; 
  } 
  res := i == 0; 
}

为什么这样修改有效？ #

1. 初始不变式成立：循环开始时i = key，显然rec_even(key) == rec_even(i)。
2. 循环体保持不变式：每次循环i减2，根据rec_even的定义，rec_even(i-2) == rec_even(i)，因此rec_even(key)依然等于rec_even(i)。
3. 循环结束推导后置条件：循环终止时i <= 1，此时：
   • 如果i == 0，res = true，而rec_even(i) = true；
   • 如果i == 1，res = false，而rec_even(i) = false。
     结合不变式rec_even(key) == rec_even(i)，就能直接推出res == rec_even(key)，满足后置条件。

内容的提问来源于stack exchange，提问作者rausted