如何在 ACSL 中编写“is power of 2”谓词？

我尝试编写一个 ACSL 谓词来查看整数是否是 2 的幂，如下所示：

/*@
  predicate positive_power_of_2 (integer i) =
    i > 0 &&
    (i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
 */

然而，当我将一些断言行添加到随机函数中时，出现一些超时（即失败）。我不明白为什么？

//@ assert positive_power_of_2 (1);  // Timeout
//@ assert positive_power_of_2 (2);  // Valid
//@ assert positive_power_of_2 (4);  // Valid
//@ assert !positive_power_of_2 (7); // Timeout

作为旁注，对于这种纯粹的逻辑属性，您可以使用lemmas 而不是assert, as in //@ lemma pow2_1: positive_power_of_2(1);。自从一个lemma是一个全局注释，它使您不必仅仅为了保存一个函数而编写一个函数assert.

现在回到问题本身。将按位运算与算术运算（小于比较）混合在一起往往会使自动定理证明者感到困惑。您没有指定使用哪一个，但如果您只使用了一个，您可能想尝试安装其他的（现在，alt-ergo、z3 和 cvc4 的混合往往会提供良好的结果）。也就是说，对 WP 内部简化器 QED 的小型交互式帮助也足够了：通过使用 GUI（请参阅第 2.4 节）工作手册 https://frama-c.com/download/frama-c-wp-manual.pdf），你可以通过展开定义来得出结论positive_power_of_2在每个目标中（据我所知，没有命令行选项可以执行相同的操作）。

基本上，一旦你进入WP ProofsGUI 面板，您必须双击Script您想要进行的证明义务对应的行的列，这将让您进入交互式证明模式，如下截图：

现在，关键是可用策略列表（右侧）是上下文相关的：仅显示与您在证明义务（左侧）中选择的术语相关的策略。有些策略总是相关的，例如Cut，它可以让您证明一个辅助陈述，该陈述可以用作其余证明中的假设，但只有在您的选择中有要展开的定义时，展开定义才有意义。因此你必须点击P_positive_power_of_2让战术出现。之后，只需点击相应的三角形即可让WP展开定义并尝试随后完成证明。