--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Double-loop invariants



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