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 回答