Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marche) · Wed, 29 Sep 2010 16:54:15 +0200

Hi,

First of all, please note that it is an english speaking list, do not 
send messages in french please.

A few remarks first:

* replace each "\forall int" by "\forall integer" and remove each cast 
"(float)" in specifications, it will avoid
   unnecessary extras casts hence might make prover's life easier

* your file is not self-contained: NULL undefined, allocM undeclared. 
replacing NULL by \null helps.

* the spec of allocM is crucial for your problems with assigns clauses 
since if you expect it to allocate a new block,
   you have to specify that.

* for me, using provers Alt-Ergo, Simplify, Z3 and CVC3, everything is 
proved except the VC corresponding
   to your main "assigns \nothing" clause. Which is not correct if 
allocM is not specified correctly.

   Try to install more provers if needed: see 
http://why.lri.fr/provers.en.html

   In particular the preservation of your loop invariants seems to be OK

Hope this helps,

- Claude

On 09/24/2010 06:04 PM, Romain Jobredeaux wrote:
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |

Frama-C-discuss mailing list archives

[Frama-c-discuss] boucles imbriquées