Dafny function-by-method无法证明后置条件问题求助

核心原因 #

Dafny的function by method机制要求method部分必须证明自身返回值与function的表达式定义完全等价，而非仅满足function的后置条件。
拆分function和method时，method只需满足自身的ensures约束即可，无需关联function的逻辑；但在function by method结构中，Dafny会强制检查两者的结果一致性——你的代码缺少建立这种等价性的关键验证条件（比如循环不变式、断言），因此无法通过验证。

以你提供的setToSequence示例为例：function的表达式直接返回[]，但method实际生成的是遍历集合后的序列，两者逻辑矛盾，Dafny自然无法确认结果等价。

解决方案 #

1. 补全验证条件，建立method与function的等价性 #

在method的循环中添加不变式，显式维护计算过程与function逻辑的关联：

function setToSequence(s: set<int>) : (r: seq<int>)
  ensures multiset(s) == multiset(r)
{
  // 改为与method逻辑等价的递归表达式
  if s == {} then [] else
    var k :| k in s;
    [k] + setToSequence(s - {k})
} by method{
  var copy := s;
  r := [];
  while copy != {}
    decreases |copy|
    // 添加不变式：已生成序列+剩余集合的多重集等于原集合
    invariant multiset(copy) + multiset(r) == multiset(s)
  {
    var k: int :| k in copy;
    r := r + [k];
    copy := copy - {k};
  }
}

这个不变式让Dafny能跟踪每一步循环后r的状态，最终证明method返回的序列与function的递归结果一致。

2. 针对tree_height这类递归function #

在遍历节点集合的循环中添加不变式，关联迭代计算的result与function的递归调用结果。例如：

• 不变式可声明当前result的值等于已处理节点的高度总和，或剩余节点的高度与result的关系，让Dafny能推导出最终result等于tree_height(t)的递归值。

3. 无表达式的function-by-method #

若不需要function的递归表达式，可将function的表达式部分留空（仅保留by method），但必须确保method能完全满足function的所有ensures约束，且通过循环不变式完成验证。

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