--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on September 2010 ---
Bonjour, Ce message fait suites aux questions d'Alwyn Goodloe de d?but juillet sur les boucles imbriqu?es et les tableaux ? dimensions multiples (qui comme on l'a fait remarquer pr?c?demment n'en sont pas vraiment, puisqu'il s'agit en fait de pointeurs doubles pointant sur un tableau de pointeurs). La fonction d'allocation passe maintenant toutes les obligations de preuves, mais nous rencontrons encore des difficult?s avec la fonction suivante, qui alloue une "matrice" de taille m,n et la remplit de 1 : /*@ requires m > 0 && n > 0; @ assigns \nothing; @ @ ensures \result == NULL || (\forall int i; \forall int j; @ 0 <= i < m && 0 <= j <n ==> *(\result[i]+j) == (float) 1.0); @*/ float** ones(int m,int n) { /*@ assert m > 0 && n > 0; */ float **c = allocM(m,n); /*@ assert (\valid(c+ (0..m-1)) && (\forall int k; 0 <= k < m ==> \valid(c[k] +(0..n-1) ) )) ; */ int i = 0; int j = 0; /*@ loop assigns *(c[0..m-1]+(0..n-1)); @ loop invariant (0 <= i <=m) && (\forall int k; \forall int q; (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0)) ; @ loop variant m-i ; */ for (i = 0; i<m; i++){ /*@ assert 0<= i < m; */ /*@ assert \valid(c[i]+(0..n-1)); */ /*@ loop assigns *(c[i] +(0..n-1)); @ loop invariant (0 <= j <= n) && (\forall int l; 0 <= l < j ==> ( *(c[i] + l) == (float)1.0) ); @ loop invariant \forall int p; \forall int q; (0 <= p <i && 0 <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ; @ loop invariant \forall int p; \forall int q; (i < p <n && 0 <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ; @ loop variant n-j ; */ for (j = 0; j<n;j++){ /*@ assert 0<=j < n ; */ /*@ assert \valid(c[i]+j); */ *(c[i] + j) = (float) 1.0; /*@ assert *(c[i] + j) == (float) 1.0; */ } /*@ assert \forall int l; 0 <= l < n ==> ( *(c[i] + l) == (float)1.0) ; */ } return c; } Seules 3 obligations de preuves ne sont pas prouvees automatiquement (parmi les 38 de default behavior), et notamment l'invariant de boucle exterieure (qui est en fait le plus important pour nous) : /*@ loop invariant (0 <= i <=m) && (\forall int k; \forall int q; (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0)) Les deux autre invariants non prouv?s concernent des conditions de type "not_assigns" sur la boucle int?rieure, et apres avoir recherch? sur google et dans les manuels des diff?rents outils je n'ai trouv? nulle part une description exacte de ce que ces conditions signifient... Pouvez-vous m'aider l? aussi ? Je suis relativement nouveau dans le domaine des methodes formelles, et dans l'usage de l'outil, je ne sais donc pas bien s'il manque simplement une anotation quelquepart, ou s'il faut faire la preuve interactivement.... Merci de votre aide, Romain Jobredeaux