Prove Length 函数统计 char 数组元素个数

Question

我试图在 C 中证明类似 strlen 的函数，但 frama-c 没有证明 post 条件和 loop variant len 子句。我不明白为什么！

我尝试过的：

/*@
    axiomatic elementNumber_axioms
    {
        logic unsigned elementNumber{L}(char *a);

        axiom elementNumber_base{L}:
            elementNumber(\null) == 0;

        axiom elementNumber_step{L}:
            \forall char *a;
            \valid(a) ==> elementNumber(a) == elementNumber(a+1) + 1;
    }
*/

/*@
    assigns \nothing;
    ensures \result == elementNumber(\old(s));
*/
unsigned stringlen(const char *s)
{
    unsigned len = 0;

/*@
    loop assigns len;
    loop assigns s;
    loop variant len;
*/
    while(*s)
    {
        ++s;
        ++len;
    }

    return len;
}

我做错了什么？

Answer 1

你写的有几个问题。一个非详尽的列表：

您的 stringlen() 不处理 s 为 NULL 的情况。

如果注释标准 C strlen() 函数，则不需要处理这种情况，因为标准 C strlen() 函数不允许参数为 NULL。但是，您的 elementNumber() 逻辑函数的公理定义将 elementNumber(\null) 定义为 0，而 stringlen() 的后置条件是结果等于 elementNumber(s)。因此，您需要处理这种情况。
stringlen() 中的 while 循环在遇到 nul 字节时终止。但是，您的 elementNumber() 逻辑函数的定义仅取决于指针是否有效。
关于s、s + 1等是否有效，stringlen()没有先决条件
您的 elementNumber() 逻辑函数未定义无效指针的值。
您将需要指定循环不变量。

我建议看一下 Frama-C 是如何注释 strlen() 的：

/*@ requires valid_string_src: valid_string(s);
  @ assigns \result \from s[0..];
  @ ensures \result == strlen(s);
  @*/
extern size_t strlen (const char *s);

strlen() 逻辑函数和 valid_string() 谓词在源代码分发的 share/libc/__fc_string_axiomatic.h 中定义，在撰写本文时为 Sodium-20150201。

Prove Length 函数统计 char 数组元素个数

Prove Length function to count char array element number

formal-verification

frama-c