I am trying to prove the below function, where the elements of the array are added by an integer value c. it's in frama c ,but i am not able to prove some parts. Can someone help with this?
#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;
}
}
Below are the unproven goals: I have highlighted the unproven goals.
[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)
You're almost there. In fact your loop invariants are not complete: you specify what happens to the beginning of the array, but not that the end stays unchanged. Generally speaking, any location mentioned in loop assigns should appear in a loop invariant, otherwise nothing is known on it after the first loop step (i.e. for proving the preservation or any annotation over a state after the loop). Here, the locations a[p..n-1] have completely unknown values except at the LoopEntry.
Adding loop invariant \forall integer i; p<= i < n ==> a[i] == \at(a[i],LoopEntry); should fix the problem.
NB: you might be tempted by a stronger loop assigns using a[0..p-1], but experience tends to show that WP is not very comfortable with loop assigns of arrays whose bound are themselves assigned. I'd suggest to add explicitely the invariant that the end of the array is unchanged.