如何在ACSL中写出"is方幂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

另外，对于这类纯粹的逻辑属性，您可以使用lemmas而不是assert，就像在//@ lemma pow2_1: positive_power_of_2(1);中那样。由于lemma是一个全局注释，因此它使您不必为了保存assert而编写函数。

现在回到问题本身。将按位运算与算术运算(小于比较)混合在一起，往往会混淆自动定理证明器。您没有指定您使用的是哪一个，但是如果您只使用一个，您可能想尝试安装其他的(现在，alt-ergo、z3和cvc4的混合使用会提供良好的结果)。尽管如此，对WP内部简化器QED的一个小的交互帮助也足够了:通过使用图形用户界面(参见可湿性粉剂手册的2.4节)，您可以通过在每个目标中展开positive_power_of_2的定义来结束(据我所知，没有命令行选项来进行等效的操作)。

基本上，一旦您在图形用户界面的WP Proofs面板中，您必须双击与要处理的证明义务相对应的行的Script列，这将允许您进入交互式验证模式，如下所示：

​

​

现在，重点是可用策略列表(在右边)是上下文的:只有那些与你在证明义务(左边)中选择的术语相关的策略。有些策略总是相关的，比如Cut，它允许您证明一个辅助语句，它可以用作其他证据中的假设，但是只有在选择中有一个定义需要展开时，展开定义才有意义。因此，你必须点击P_positive_power_of_2让战术出现。然后，只需点击相应的三角形，让WP展开定义，然后尝试完成证明。