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] Loop invariants with imbricated loops.

Le mer. 20 mai 2009 15:17:29 CEST,
JENN Eric <eric.jenn at fr.thalesgroup.com> a ?crit :

> Me, again.
> Consider the following code:
> 
> void test1() {

//...

>   {
>     /*@ loop invariant 0 <= b <= 3;
>         loop invariant
>       \forall integer j;
>         ( 0 <= j < b ) ==> (the_array[a+j*3] == -1);
>       @*/
>     for ( b = 0; b< 3 ; b++)
>     {
>       the_array[a+b*3] = -1;
>     }
> 
>     /*@
>       assert
>       \forall integer j;
>             ( 0 <= j < 3 ) ==> (the_array[a+j*3] == -1);
>         @*/
>   }
> }
> 
> All POs corresponding to the invariants of the inner-most loop, and the assertion, are discharged.
> The PO corresponding to the preservation of invariant of the outer-most is demonstrated not to be valid... and I don't understand why?

Because, the loop invariant of the inner loop is too weak: you specify
what happens on the a-th 'column' of the array, but not that the
preceding ones are left untouched by the loop. And since the loop
annotation is the only thing that jessie sees outside of the loop,
there is nothing in the hypotheses of the PO that says that these
'columns' still contain -1.
Now the standard ACSL way of specifying that would be a via loop assigns
(left as an exercise for the reader). However, since loop assigns are
not handled by the current version of the jessie plugin, a work-around
must be found in the form of another invariant:
        loop invariant
        \forall integer i,j;
        (0<=i <a) && (0<=j<3) ==> the_array[i+j*3] == -1;

> In particular, the assertion is demonstrated to be  TRUE for all a in [0,3[ so, doesn't this guarantee the preservation of the outer-most invariant?

No, for the same reason as above: the assertion talks about the a-th
'column'.

As a final note, note that the outer loop invariant seem to be handled
more easily by ATP when it is written in this form:
     loop invariant
      \forall integer i,j;
        ( 0 <= i < a ) && (0<=j<3) ==>
          (the_array[i+j*3] == -1);

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile