对于整数对数使用什么循环不变式？

Question

由于我正在用Frama-C进行C形式验证的第一步，所以我试图正式验证如下编写的整数二进制对数函数：

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    while (n > 1) {
        n /= 2;
        ++res;
    }
    return res;
}

我正在使用Frama-C 20.0（钙），并带有命令frama-c-gui -rte -wp file.c（由于某种原因，我没有Jessie插件）。我已经检查了保持n = 100,000,000的后置条件（使用标准库断言），但是尽管我已尽力而为，但此函数仍未正式验证，并且Frama-C教程通常涉及琐碎的循环变体（而不是每次迭代减半），因此与我要尝试的结果不太接近。

我尝试了以下代码注释，其中一些可能是不必要的：

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    /*@
        loop invariant 0 < n <= \at(n, Pre);
        loop invariant \at(n, Pre) < n * pow2(res + 1);
        loop invariant pow2(res) <= \at(n, Pre);
        loop invariant res > 0 ==> 2 * n <= \at(n, Pre);
        loop invariant n > 1 ==> pow2(res + 1) <= \at(n, Pre);
        loop invariant res <= pow2(res);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        n /= 2;
        //@ assert 2 * n <= \at(n, L);
        ++res;
        //@ assert res == \at(res, L) + 1;
    }
    //@ assert n == 1;
    return res;
}

无法验证的注释是循环不变式2和5（Alt-Ergo 2.3.0和Z3 4.8.7超时）。就不变式2而言，难度似乎与整数除法有关，但我不确定为使WP能够证明这一点而增加了什么。至于不变量5，WP可以证明它已经建立，但是不能被保留。它可能需要一个能够捕获当n变为1时发生的情况的属性，但是我不确定什么可以工作。

我如何指定缺少的信息来验证这些循环不变式，是否有另一个Frama-C分析可以使我更轻松地找到循环不变式？

谢谢您的考虑。

Answer 1

作为一般说明，通常为您的注释命名是一个好主意，尤其是当您开始对同一循环使用多个循环不变式时。它可以让您更快地找出失败的名称（尽管您可以随意不同意我选择的名称，但请参见以下示例）。

现在回到您的问题：重点是您的不变式2太弱了。如果当前循环中的n为奇数，则无法确定不等式在下一步中成立。有了更严格的界限，即\at(n,Pre) < (n+1) * pow2(res)，假设我们知道res不会溢出，那么当前步骤开始时的假设就足以证明不变量在步骤结束时成立。最终将变为1+res，并且不等式将不再成立。

为此，我使用了中间幻影函数来证明0任何n < pow2(n)，由于下面的unsigned不变式，因此允许我确保通过任何循环步骤保留pow2_lower。

最后，对res_bound的简短说明：此处无关紧要，因为参数为pow2，因此非负，但是在一般情况下，unsigned参数可以为负，因此您可能需要通过在integer时返回1，使定义更加健壮。

总而言之，以下程序已完全用Frama-C 20和Alt-Ergo（n<=0）证明。似乎还需要两个断言来指导Alt-Ergo进行其证据搜索。

frama-c -wp -wp-rte file.c