无法验证分配子句 - Frama-C
Unable to verify assign clause - Frama-C
在我下面的示例中,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)
我只是在这个程序中以相反的顺序将数组归零。
您缺少 i
上的循环不变量。因此,WP 不知道它可以取值的范围,也无法证明正在写入的 a
的索引是 0 .. n-1
。只需添加
@ loop invariant -1 <= i <= n-1;
(请注意,在最后一次迭代结束时,i
是 -1
,而不是 0
。)
在我下面的示例中,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)
我只是在这个程序中以相反的顺序将数组归零。
您缺少 i
上的循环不变量。因此,WP 不知道它可以取值的范围,也无法证明正在写入的 a
的索引是 0 .. n-1
。只需添加
@ loop invariant -1 <= i <= n-1;
(请注意,在最后一次迭代结束时,i
是 -1
,而不是 0
。)