如何为Dafny中高阶递归函数funpow编写合法前置条件？

针对你编写funpow函数时遇到的前置条件验证失败、裸函数错误问题，可通过以下方案解决：

问题根源 #

1. 原前置条件forall i :: 0 <= i < n ==> f.requires(funpow(i,f,t))存在循环依赖：Dafny无法自动证明funpow(i,f,t)的前置条件成立，而该条件本身又依赖于这个全称量词断言。
2. 直接引用funpow.requires触发“裸函数”错误，是因为Dafny禁止递归函数在自身前置条件中直接引用自身的requires属性，避免陷入无限验证循环。

解决方案：简化前置条件+归纳引理证明全称性质 #

步骤1：简化funpow的前置条件 #

只保证递归步骤的合法性，避免直接引用自身的requires：

function funpow<T(!new)>(n: nat, f: T ~> T, t: T): T
  requires n == 0 || f.requires(funpow(n-1, f, t))
  reads f.reads
  decreases n
{
  if n == 0
  then t
  else f(funpow(n-1, f, t))
}

这个前置条件仅要求：当n>0时，f可以安全应用到funpow(n-1,f,t)的结果上，Dafny可通过递归递减规则自动验证该条件。

步骤2：编写归纳引理证明全称前置条件 #

如果需要你最初想要的“所有0<=i<n都满足f.requires(funpow(i,f,t))”的性质，可编写归纳引理来证明：

lemma LemmaFunpowAllPreconditions<T(!new)>(n: nat, f: T ~> T, t: T)
  requires funpow.requires(n, f, t)
  ensures forall i :: 0 <= i < n ==> f.requires(funpow(i, f, t))
  reads f.reads
{
  if n == 0 {
    // 空量词范围，无需额外证明
  } else {
    // 递归调用引理，证明n-1的情况
    LemmaFunpowAllPreconditions(n-1, f, t);
    // 由funpow的前置条件，直接得到n-1时的f.requires成立
    assert f.requires(funpow(n-1, f, t));
  }
}

在需要使用全称前置条件的场景中，调用该引理即可自动推导出所需断言。

替代方案：使用辅助谓词 #

也可以定义辅助谓词描述“f可连续应用k次到t”的性质，以此作为funpow的前置条件：

predicate CanApplyKTimes<T(!new)>(k: nat, f: T ~> T, t: T)
  reads f.reads
{
  k == 0 || (CanApplyKTimes(k-1, f, t) && f.requires(funpow(k-1, f, t)))
}

function funpow<T(!new)>(n: nat, f: T ~> T, t: T): T
  requires CanApplyKTimes(n, f, t)
  reads f.reads
  decreases n
{
  if n == 0 then t else f(funpow(n-1, f, t))
}

该谓词通过递归定义连续应用的合法性，Dafny可自动验证其与funpow递归逻辑的一致性。

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