《ANSI/ISO C规范语言版本1.23：在Frama-C 32.1中实现》附录A.2描述了一个内置函数 integer pow(integer x, integer y) ;（奇怪的是，它缺少前导的 \）。但 logic_builtin.ml（https://git.frama-c.com/pub/frama-c/-/blob/stable/germanium/src/kernel_internals/typing/logic_builtin.ml）显示 pow 作为接收 doubles，而不是 integers。这里的预期行为是什么？文档和实现中是否有一个或两个不正确？我有点怀疑：a) 应该存在一个带前导斜杠的 integer 对 \pow 的重载；b) 文档中有一个笔误，遗漏了斜杠；c) 实现缺少这个重载；d) 现有的 pow 实现是C 标准库函数，在某种程度上与A.2的定义并行（尽管也许值得在那里也包括）。是否有比

logic integer Pow2(integer k) =
    k <= 0 ? 1 : 2 * Pow2(k - 1);

更好的方式来表示一个 integer 2^k操作，若 pow(2, k) 确实不可用？

解决方案

确实存在一些与此主题相关的逻辑内置函数的问题。命名和类型上的不一致性，外加一些当前尚未文档化的内置函数。

考虑在WP中表示pow2操作以用于证明的问题，没有一个完美的答案：这在很大程度上取决于你想证明的性质。目前，WP对位相关运算的处理被卡在两个不兼容的约束之间：

• 它被用于位表示通常无用的系统，因此相关考量通常被忽略，Qed为提升性能对所有算术运算进行大幅简化，
• 在推理中处理位运算需要尽量保持表达式原样，以最大限度提高SMR求解器将其匹配并用以处理验证条件的机会。

目前，WP更偏向第一方向，因为从历史上看，这也是最常见的工业用例。

如果你想用WP来研究这类问题，最好的做法是联系开发者。