loops - 无法验证分配子句 - Frama-C

Question

在我下面的示例中，frama-c 无法证明我在函数契约中的赋值子句，我不确定为什么。如果有任何帮助，我将不胜感激。

/*@
  @ requires n>0;
  @ requires \valid(a+(0..n-1));
  @ ensures \forall int i; (n>i>=0 ==> a[i]==0);
  @*/

 void f(int n, float *a) {
     /*@ 
       @ loop invariant n>=0;
       @ loop invariant test: \forall int j; (n>j>i ==> a[j]==0);
       @ loop assigns i, a[0..n-1];
       @*/
     for (int i=n-1; i>=0; i--) {
         a[i] = 0;
     }

 }

这是我的输出:

[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_loop_assign_part3 : Unknown (Qed:24ms) (406ms)
[wp] Proved goals:    7 / 8
    Qed:             5  (4ms-13ms-24ms)
    Alt-Ergo:        2  (20ms-32ms) (28) (unknown: 1)

我只是在这个程序中以相反的顺序将数组归零。

Answer 1

您缺少 i 上的循环不变量。因此，WP 不知道它可以取值的范围，也无法证明正在写入的 a 的索引是 0 .. n-1 .只需添加

   @ loop invariant -1 <= i <= n-1;

(注意在最后一次迭代结束时，i 是-1，而不是0。)