c - 什么循环不变量用于整数对数？

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 (Calcium)，命令为 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 使定义更可靠每当n<=0 .

总而言之，以下程序完全通过 Frama-C 20 和 Alt-Ergo ( frama-c -wp -wp-rte file.c ) 得到证明。似乎仍然需要两个断言来指导 Alt-Ergo 的证明搜索。

#include "stddef.h"

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

/*@ ghost
/@ assigns \nothing;
   ensures n < pow2(n);
@/
void lemma_pow2_bound(unsigned n) {
  if (n == 0) return;
  lemma_pow2_bound(n-1);
  return;
}
*/

/*@
    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 n_bound: 0 < n <= \at(n, Pre);
        loop invariant pow2_upper: \at(n, Pre) < (n+1) * pow2(res);
        loop invariant pow2_lower: n*pow2(res) <= \at(n, Pre);
        loop invariant res_bound: 0 <= res < \at(n,Pre);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        /*@ assert n % 2 == 0 || n % 2 == 1; */
        n /= 2;
        /*@ assert 2*n <= \at(n,L); */
        res++;
        /*@ ghost lemma_pow2_bound(res); */
    }
    //@ assert n == 1;
    return res;
}