--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] boucles imbriquées



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