Dafny中EquivalentSpec'报Resolution Failed，EquivalentSpec正常，求原因

你的代码里，EquivalentSpec能通过验证是因为：当你把两个方法的返回值赋值给变量a和b时，Dafny会自动将方法的后置条件绑定到变量上——a被约束为a == 3*x，b则满足Average(b, 3*x) == 3*x和b%3 == 0。解Average(b, 3*x) == 3*x这个等式可得b = 3*x，再结合b%3 == 0的条件（这里是冗余约束），就能直接推导出a == b，所以验证通过。

而EquivalentSpec'中的assert Triple(x) == Triple'(x)验证失败，并非Dafny的bug，而是因为Dafny不会在逻辑断言中自动展开方法的后置条件来推导等式。在逻辑断言里直接写方法调用时，验证器不会主动关联方法的规范（比如Triple的ensures r == 3*x）来替换方法调用，它无法直接识别两个方法调用的返回值满足相同的约束。

可行的解决方式 #

要让EquivalentSpec'通过验证，你需要显式地把方法的规范转化为逻辑层面的约束，最直接的方式就是用中间变量捕获返回值（也就是你觉得“不够自然”的EquivalentSpec写法，这其实是Dafny验证这类等价性的常规做法）。如果你想简化，也可以在方法里显式基于规范推导：

method EquivalentSpec'(x: int)
{
  var a := Triple(x);
  var b := Triple'(x);
  // 显式引用方法的后置条件辅助推导
  assert a == 3*x;
  assert (b + 3*x)/2 == 3*x; // 展开Average的定义和Triple'的ensures
  assert b == 3*x;
  assert a == b;
}

本质上，Dafny对程序构造（方法调用）和逻辑构造（断言）的处理逻辑不同：方法是可执行的代码实体，而逻辑断言需要明确的逻辑约束链来完成推导，不会自动隐式地将方法的规范映射到逻辑断言中的方法调用上。

内容的提问来源于stack exchange，提问作者A. Meijster