Loops 无法验证assign子句-Frama-C

Loops 无法验证assign子句-Frama-C,loops,automated-tests,proof,frama-c,Loops,Automated Tests,Proof,Frama C,在我下面的示例中,frama-c无法证明函数契约中的assign子句,我不知道为什么。我真的很感激任何帮助 /*@ @ 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;

在我下面的示例中,frama-c无法证明函数契约中的assign子句,我不知道为什么。我真的很感激任何帮助

/*@
  @ 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)

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

I
上缺少一个循环不变量。因此,WP不知道它可以取值的范围,也无法证明正在编写的
a
的索引是
0。。n-1
。加上

   @ loop invariant -1 <= i <= n-1;
循环不变量-1