frama-c - 如何在 ACSL 中编写 "is power of 2"谓词？

Question

我尝试编写 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

Answer 1

作为旁注，对于这种纯粹的逻辑属性，您可以使用 lemma s 而不是 assert ，如 //@ lemma pow2_1: positive_power_of_2(1); .自 lemma是一个全局注解，它让你不必为了持有 assert 而编写函数。 .
现在回到问题本身。将按位运算与算术运算(小于比较)混合使用往往会混淆自动定理证明器。您没有指定使用哪一个，但如果您只使用了一个，您可能想尝试安装其他的(现在，alt-ergo、z3 和 cvc4 的组合往往会提供良好的结果)。也就是说，对 WP 的内部简化器 QED 的小型交互式帮助也足够了:通过使用 GUI(请参阅 WP manual 的第 2.4 节)，您只需展开 positive_power_of_2 的定义即可得出结论。在每个目标中(据我所知，没有命令行选项可以执行等效操作)。
基本上，一旦你在 WP Proofs GUI 的面板，您必须双击 Script您要处理的证明义务对应的行的列，这将让您进入交互证明模式，如下图所示:

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