frama-c - 证明 Length 函数计算 char 数组元素个数

Question

我试图在 C 中证明类似 strlen 的函数，但 frama-c 不证明后置条件和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() 逻辑函数的定义仅取决于指针是否有效。

• stringlen() 没有关于 , 等是否有效的先决s条件s + 1。

• 您的 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。