# 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.

*Subject*: [Frama-c-discuss] Loop invariants with imbricated loops.*From*: virgile.prevosto at cea.fr (Virgile Prevosto)*Date*: Wed, 20 May 2009 17:25:21 +0200*In-reply-to*: <4A1402E9.8090307@fr.thalesgroup.com>*References*: <4A1402E9.8090307@fr.thalesgroup.com>

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

**Follow-Ups**:**[Frama-c-discuss] Loop invariants with imbricated loops.***From:*dragan.stosic at gmail.com (Dragan)

**References**:**[Frama-c-discuss] Loop invariants with imbricated loops.***From:*eric.jenn at fr.thalesgroup.com (JENN Eric)

- Prev by Date:
**[Frama-c-discuss] Loop invariants with imbricated loops.** - Next by Date:
**[Frama-c-discuss] String results in logical specifications** - Previous by thread:
**[Frama-c-discuss] Loop invariants with imbricated loops.** - Next by thread:
**[Frama-c-discuss] Loop invariants with imbricated loops.** - Index(es):