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
4

1 回答 1

2

作为旁注，对于此类纯逻辑属性，您可以使用lemmas 代替assert，如//@ lemma pow2_1: positive_power_of_2(1);. 由于 alemma是一个全局注解，它使您不必仅仅为了保存一个assert.

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

基本上，一旦你进入了 GUI 的面板，你必须在你想要处理的证明义务对应的行WP Proofs的列中双击，这将让你进入交互证明模式，如下图所示：Script

Frama-C GUI 中的 WP 交互式打样模式

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

于 2020-10-09T08:03:34.473 回答