--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on April 2009 ---
Here's a formally expressed version of yesterday's quizz: int t[100]; /*@ requires \forall integer k ; 0 <= k < 100 ==> t[k] == 1 ; ensures \forall integer k ; 0 <= k < 100 ==> t[k] == 2 ; */ void f(void) { int i; /* write your invariant here */ for (i=0; i<100; i++) t[i]++; } and my proposed solution is a couple of pages below for those who want to see it: /*@ loop invariant (0 <= i <= 100) && (\forall integer k ; 0 <= k < i ==> t[k] == 2) && (\forall integer k ; i <= k < 100 ==> t[k] == 1) ; */ The loop invariant needs to remember everything that has already been done (the (\forall integer k ; 0 <= k < i ==> t[k] == 2) part) and all the information that will be necessary to make sense of the next iterations, i.e. the fact that the untouched cells still contain 1; that's the (\forall integer k ; i <= k < 100 ==> t[k] == 1) part. Pascal -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090403/03077d83/attachment.htm