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

当我开始使用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-gui -rte -wp file.c使用Frama-C 20.0（Calcium）（由于某种原因，我没有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分析可以使我更轻松地找到循环不变式？

谢谢您的考虑。

最佳答案

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

现在回到您的问题：重点是您的不变式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进行其证据搜索。

#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;
}

关于c - 整数对数使用什么循环不变式？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/60161173/