有什么方法可以在 frama C 中指定循环内的先决条件?
any way to specify preconditions inside loop in frama C?
我试图证明下面的函数,其中数组的元素与整数值 c 相加。
它在 frama c 中,但我无法证明某些部分。
有人可以帮忙吗?
#include <limits.h>
/*@requires n>0;
requires \forall integer i;0<=i<n ==> INT_MIN<=a[i]+c<=INT_MAX;
requires \valid(a+(0..n-1));
ensures \forall integer i;0<=i<n ==> a[i] == \old(a[i]) +c;
assigns a[0..n-1];
*/
void array(int *a,int n,int c){
/*@loop invariant 0<=p<=n;
loop invariant \forall integer i;0<=i<p ==> a[i] == \at(a[i],LoopEntry) +c;
loop assigns p,a[0..n-1];
loop variant n-p;
*/
for(int p=0;p<n;p++){
a[p]=a[p]+c;
}
}
以下是未经证实的目标:
我已经强调了未经证实的目标。
[kernel] Parsing q2.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function array
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_array_loop_invariant_established : Valid (8ms)
[wp] [Qed] Goal typed_array_loop_invariant_2_established : Valid (5ms)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_2_preserved : Timeout (Qed:43ms) (10s) (cached)<----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_preserved : Valid (Qed:40ms) (32ms) (12) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_ensures : Valid (Qed:35ms) (50ms) (52) (cached)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_2 : Timeout (Qed:16ms) (10s) (cached)<-----
------>[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow : Timeout (Qed:17ms) (10s) (cached)<-----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access_2 : Valid (Qed:18ms) (45ms) (112) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access : Valid (Qed:71ms) (44ms) (109) (cached)
[wp] [Qed] Goal typed_array_assigns : Valid (4ms)
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_variant_positive : Valid (13ms)
[wp] [Qed] Goal typed_array_loop_variant_decrease : Valid (15ms)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_assigns_part2 : Valid (Qed:27ms) (59ms) (139) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_3 : Valid (Qed:93ms) (37ms) (62) (cached)
[wp] [Cache] found:9
[wp] Proved goals: 12 / 15
Qed: 6 (4ms-30ms-93ms)
Alt-Ergo 2.3.3: 6 (32ms-59ms) (139) (interrupted: 3) (cached: 9)
你快到了。事实上,您的循环不变量并不完整:您指定数组开头发生的情况,但不是结尾保持不变。一般来说,loop assigns
中提到的任何位置都应该出现在 loop invariant
中,否则在第一个循环步骤之后就什么都不知道了(即用于证明保存或在循环后状态上的任何注释)。在这里,位置 a[p..n-1]
具有完全未知的值,除了 LoopEntry
.
添加 loop invariant \forall integer i; p<= i < n ==> a[i] == \at(a[i],LoopEntry);
应该可以解决问题。
注意:您可能会被使用 a[0..p-1]
的更强大的 loop assigns
所吸引,但经验往往表明 WP 对数组的循环赋值不太舒服,数组的边界是自己赋值的。我建议明确地添加数组末尾不变的不变量。
我试图证明下面的函数,其中数组的元素与整数值 c 相加。 它在 frama c 中,但我无法证明某些部分。 有人可以帮忙吗?
#include <limits.h>
/*@requires n>0;
requires \forall integer i;0<=i<n ==> INT_MIN<=a[i]+c<=INT_MAX;
requires \valid(a+(0..n-1));
ensures \forall integer i;0<=i<n ==> a[i] == \old(a[i]) +c;
assigns a[0..n-1];
*/
void array(int *a,int n,int c){
/*@loop invariant 0<=p<=n;
loop invariant \forall integer i;0<=i<p ==> a[i] == \at(a[i],LoopEntry) +c;
loop assigns p,a[0..n-1];
loop variant n-p;
*/
for(int p=0;p<n;p++){
a[p]=a[p]+c;
}
}
以下是未经证实的目标: 我已经强调了未经证实的目标。
[kernel] Parsing q2.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function array
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_array_loop_invariant_established : Valid (8ms)
[wp] [Qed] Goal typed_array_loop_invariant_2_established : Valid (5ms)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_2_preserved : Timeout (Qed:43ms) (10s) (cached)<----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_preserved : Valid (Qed:40ms) (32ms) (12) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_ensures : Valid (Qed:35ms) (50ms) (52) (cached)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_2 : Timeout (Qed:16ms) (10s) (cached)<-----
------>[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow : Timeout (Qed:17ms) (10s) (cached)<-----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access_2 : Valid (Qed:18ms) (45ms) (112) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access : Valid (Qed:71ms) (44ms) (109) (cached)
[wp] [Qed] Goal typed_array_assigns : Valid (4ms)
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_variant_positive : Valid (13ms)
[wp] [Qed] Goal typed_array_loop_variant_decrease : Valid (15ms)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_assigns_part2 : Valid (Qed:27ms) (59ms) (139) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_3 : Valid (Qed:93ms) (37ms) (62) (cached)
[wp] [Cache] found:9
[wp] Proved goals: 12 / 15
Qed: 6 (4ms-30ms-93ms)
Alt-Ergo 2.3.3: 6 (32ms-59ms) (139) (interrupted: 3) (cached: 9)
你快到了。事实上,您的循环不变量并不完整:您指定数组开头发生的情况,但不是结尾保持不变。一般来说,loop assigns
中提到的任何位置都应该出现在 loop invariant
中,否则在第一个循环步骤之后就什么都不知道了(即用于证明保存或在循环后状态上的任何注释)。在这里,位置 a[p..n-1]
具有完全未知的值,除了 LoopEntry
.
添加 loop invariant \forall integer i; p<= i < n ==> a[i] == \at(a[i],LoopEntry);
应该可以解决问题。
注意:您可能会被使用 a[0..p-1]
的更强大的 loop assigns
所吸引,但经验往往表明 WP 对数组的循环赋值不太舒服,数组的边界是自己赋值的。我建议明确地添加数组末尾不变的不变量。