--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Solution to yesterday's quizz



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