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
- Prev by Date: [Frama-c-discuss] Looking for paper describing Frama-C internals
- Next by Date: [Frama-c-discuss] Calculation of SW complexity
- Previous by thread: [Frama-c-discuss] Calculation of SW complexity
- Next by thread: [Frama-c-discuss] boucles imbriquées
- Index(es):