3

由于我正在使用 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 分析可以让我更轻松地找到循环不变量？

谢谢您的考虑。

4

1 回答 1

2

作为一般评论，命名注释通常是一个好主意，尤其是当您开始为同一个循环设置多个循环不变量时。它将允许您更快地查明失败的那些（请参见下面的示例，尽管您可以自由地不同意我选择的名称）。

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

为此，我使用了一个中间的 ghost 函数来证明n < pow2(n)对于 any unsigned，由于pow2_lower下面的不变量，我可以确保它res_bound被任何循环步骤保留。

最后，关于 的一个小评论pow2：这里没关系，因为参数是unsigned，因此是非负的，但在一般情况下，参数可以是负的，integer因此您可能希望通过返回来使定义更加健壮。1n<=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;
}
于 2020-02-12T08:59:13.080 回答