--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on February 2011 ---
Hi, Like a few days ago, I am trying to prove some loop-related C code with the jessie plugin. Now I am working on a double loop that sets the values of a matrix as the sum of two others matrix. Here is my code: typedef struct { int a[2][2]; int b[2][2]; int Sum[2][2]; } t_matrix; t_matrix mat; /*@ predicate disjoint_matrix(t_matrix* s) = \forall integer m; 0 <= m < 2 ==> \valid_range(s->a[m],0,1) && \valid_range(s->b[m],0,1) && \valid_range(s->Sum[m],0,1) && \forall integer m,n,o,p; 0 <= m < 2 && 0 <= n < 2 && 0 <= o < 2 && 0 <= p < 2 ==> s->a[m]+n != s->Sum[o]+p && s->b[m]+n != s->Sum[o]+p; */ /*@ requires disjoint_matrix(&mat); assigns mat.Sum[0..1][0..1]; */ void f(){ int i = 0; int j = 0; Init: /*@ loop invariant 0 <= i <= 2; loop invariant 0 <= j <= 2; loop invariant \forall integer m,n; i <= m < 2 && 0 <= n < 2 ==> mat.Sum[m][n] == \at(mat.Sum[m][n],Init); //(1) loop invariant \forall integer m,n; 0 <= m < i && 0 <= n < 2 ==> mat.Sum[m][n] == mat.a[m][n] + mat.b[m][n]; //(2) loop assigns i,j,mat.Sum[0..i-1][0..j-1]; loop variant 2-i; */ for (i=0; i < 2; i++) { FirstLoop: /*@ loop invariant 0 <= j <= 2; loop invariant 0 <= i <= 2; loop invariant \forall integer n; j <= n < 2 ==> mat.Sum[i][n] == \at(mat.Sum[i][n],FirstLoop); //(6) loop invariant \forall integer n; 0 <= n < j ==> mat.Sum[i][n] == mat.a[i][n] + mat.b[i][n]; loop invariant \forall integer m,n; 0 <= m < i && 0 <= n < 2 ==> mat.Sum[m][n] == mat.a[m][n] + mat.b[m][n]; //(3) loop invariant \forall integer m,n; i < m < 2 && 0 <= n < 2 ==> mat.Sum[m][n] == \at(mat.Sum[m][n],FirstLoop); //(4) loop assigns j,mat.Sum[i][0..j-1]; loop variant 2-j; */ for (j=0; j < 2; j++){ mat.Sum[i][j] = mat.a[i][j] + mat.b[i][j]; } } } I prove thanks to the predicate that all the a and b matrix elements are disjoint in memory of the Sum matrix. When I try to prove it the (3) and (4) invariants are not proven. I also tried to add some assertion in the last loop like this: for (j=0; j < 2; j++){ //@ assert \forall integer n; 0 <= n < j ==> mat.Sum[i][n] == mat.a[i][n] + mat.b[i][n]; //@ assert \forall integer n; j <= n < 2 ==> mat.Sum[i][n] == \at(mat.Sum[i][n],FirstLoop); mat.Sum[i][j] = mat.a[i][j] + mat.b[i][j]; //@ assert \forall integer n; 0 <= n <= j ==> mat.Sum[i][n] == mat.a[i][n] + mat.b[i][n]; //@ assert \forall integer n; j < n < 2 ==> mat.Sum[i][n] == \at(mat.Sum[i][n],FirstLoop); } I tried this to add some kind of induction in my proof but it does not works. Some questions are bothering me: 1 - I saw that it's not possible to access a C label if an other one is between (impossible to set the \at to Init in the 6 invariant), is it normal ? 2 - Is it necessary, in order to prove the invariants, to repeat the invariants in each loop level (like I did with 1,2 repeated in 3 and 4) ? 3 - I think I have put everything I could to prove this but I do not succeed, do anyone have an idea ? Arnaud