formal-verification - 在Why3的谓词中调用我自己的函数

Question

使用最新版本的 Why3 (1.0.0)，当我尝试执行以下操作时：

 let add_one (n: int) : int = n+1
 predicate is_successor_of (n: int) (m: int) = m = add_one n

我收到以下形式的错误：文件“../something.why”，第 x 行，字符 yz：未绑定符号 'add_one'。难道我做错了什么？我看到的大多数WhyML 代码示例实际上仅使用内置/标准库函数，但确实调用了同一文件中定义的其他谓词。在定义谓词时，是否没有类似的方法来调用我在同一个文件中定义的函数？

Answer 1

使用关键字将原始add_one函数定义标记为纯函数function似乎可以解决问题。这是有道理的，因为在谓词中不应允许副作用。