如何在 ACSL 中编写“是 2 的幂”谓词？答案

【问题标题】：How do I write an "is power of 2" predicate in ACSL?如何在 ACSL 中编写“是 2 的幂”谓词？
【发布时间】：2020-10-08 18:14:50
【问题描述】：

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

【问题讨论】：

标签： frama-c acsl

【解决方案1】：

附带说明，对于此类纯逻辑属性，您可以使用lemmas 代替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 的定义来得出结论（到目前为止据我所知，没有命令行选项可以做到这一点）。

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

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

【讨论】：

alt-ergo 2.2.0，但我也安装了 z3 和 gappa（由于我无法理解的原因，它似乎总是更喜欢 alt-ergo）。
您能否扩展您所说的“您可以通过展开每个目标中 positive_power_of_2 的定义来得出结论”？这到底是在 GUI 中的什么位置？
当然。 WP 的交互式证明界面至少可以说不是我见过的最符合人体工程学的软件。我希望我的解释是足够的，恐怕我需要一个完整的视频而不是单个图像才能使事情尽可能清晰。
是的，我能够以这种方式证明小常数 N 的简单 is-power-of-2(N)。我这样做是为了证明一个实际的 C 函数，但我要为此提出一个新问题。