在 Frama-C 中证明 while 循环

Question

我正在尝试用 frama-c 中的指针赋值来证明 while 循环。不幸的是，我遇到了问题。如果用 for 循环和数组符号重写被测代码，我已经设法证明了这一点。有人知道如何证明这一点吗？

我要证明的代码：

/*@
 requires \valid(v+(0..n-1));
 requires v != \null;
 requires n > 0;
 assigns v[0..n-1];
 ensures \forall integer q; 0<=q<=n-1 ==> v[q]==(unsigned char)0;
*/
static void make_zero( unsigned char *v, size_t n ) {

volatile unsigned char *p = (unsigned char*)v;

      /*@
       loop invariant 0 <= n <= \at(n, Pre);
       loop invariant \forall integer j;  0 <= j < (\at(n, Pre)-n) ==> \at(p, Pre)[j] == (unsigned char)0;
       loop assigns n, p;
       loop variant n;  */

      while( n-- ){
         *p++ = 0;
      }
 }

重写代码：

/*@
loop invariant 0 <= i <= n;
loop invariant \forall integer j; 0 < j < i ==> p[j] == (unsigned char)0;
loop assigns i, p[0..n-1];
loop variant n-i;
*/

for(size_t i = 0; i<n; i++){
  p[i] = 0;
}

Answer 1

首先，请注意。前置条件 v != \null 与 \valid(v+(0..n-1)) 是多余的，可以删除。

另外，p 是一个局部变量，它不在 Pre 状态的范围内。因此 \at(p, Pre) 或多或少是没有意义的（尽管被 WP 接受）。您的意思可能是 v - 无论如何更简单。

其次，您的循环赋值是错误的。 v指向的数组的单元格也被修改。您必须将其更改为 assigns n, p, v[0..\at(n, Pre)-n-1].

第三，您需要另一个循环不变量，它用 v 和 n 表示 p。否则，WP 将无法准确模拟写入 *p 时发生的情况，也无法证明修改后的 loop assigns。这个不变量是 p == v + (\at(n, Pre)-n).

您的最后一个问题是您声明了 p volatile。这在这里是不需要的，实际上使证明变得不可能：p 的值可能会在每次访问时发生变化。删除此限定符后，证明就完成了。

完整代码供参考：

/*@
 requires \valid(v+(0..n-1));
 requires n > 0;
 assigns v[0..n-1];
 ensures \forall integer q; 0<=q<=n-1 ==> v[q]==(unsigned char)0;
*/
static void make_zero( unsigned char *v, size_t n ) {

  unsigned char *p = (unsigned char*)v;

  /*@
    loop invariant 0 <= n <= \at(n, Pre);
    loop invariant p == v+(\at(n, Pre)-n);
    loop invariant \forall integer j;  0 <= j < (\at(n, Pre)-n) ==> v[j] == (unsigned char)0;
    loop assigns n, p, v[0..\at(n, Pre)-n-1];
    loop variant n;
  */

  while( n-- ){
    *p++ = 0;
  }
}

在 Frama-C 中证明 while 循环

Prove while-loop in Frama-C

frama-c