Dafny中函数对称性证明失败且报终止性错误求助

• 核心错误：混用function和method关键字
  Dafny里function和method是完全不同的声明类型：

  • function用于定义无副作用的纯数学函数，Dafny会自动处理非递归函数的终止验证，且支持逻辑推理证明后置条件
  • method用于命令式代码，允许存在副作用，即使非递归也会触发严格的终止检查逻辑

  你写的function method是非法的关键字组合，这直接导致Dafny误判了代码类型，抛出终止证明的错误。

• 修正后的可验证代码
  把错误的function method改成纯function，示例代码就能正常通过验证：

  function dummy(a: real, b: real): real
      ensures dummy(a, b) == dummy(b, a)
  {
      a * b
  }
  

  此时Dafny会识别这是无递归的纯函数，自动跳过终止检查；同时因为实数乘法的交换律是Dafny内置的公理，后置条件dummy(a,b) == dummy(b,a)会被直接验证通过。

• 针对复杂函数的补充提示
  如果你的真实函数是递归结构，需要手动添加decreases子句指定终止度量（比如递归参数的规模递减），帮助Dafny证明终止性；而对称性的证明如果涉及复杂逻辑，可能需要额外添加辅助引理（lemma）来拆解证明步骤。

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