Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] boucles imbriquées

  • Subject: [Frama-c-discuss] boucles imbriquées
  • From: Romain.Jobredeaux at supelec.fr (Romain Jobredeaux)
  • Date: Fri, 24 Sep 2010 18:04:10 +0200
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