--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on May 2009 ---
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