如何在Dafny中定义无函数体的验证用函数？

Dafny中普通function要求必须包含实现体，因此你写的代码会报错。若要定义仅依靠前置/后置条件用于验证的无体函数，有两种正确方式：

方式一：使用ghost函数 #

ghost函数仅用于验证逻辑，不参与实际执行，无需实现体：

ghost function test(n: nat): (m: nat)
   ensures m == n+1

方式二：使用公理函数 #

通过{:axiom}属性标记函数，Dafny会直接信任其规范的正确性（注意：滥用公理可能引入逻辑不一致，需谨慎使用）：

function {:axiom} test(n: nat): (m: nat)
   ensures m == n+1

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