--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2009 ---
You can also have a look at the sorting example in the tutorial: http://frama-c.cea.fr/jessie_tutorial_index.html I know, it is only given "as is" and it needs to be explained, but I hope it helps anyway. - Claude Virgile Prevosto wrote: > Hello Kerstin, > > Le mer. 03 juin 2009 13:43:48 CEST, > "Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit : > >> the array are growing. There's always a problem with the loop >> invariants. The post conditions are valid. > > Just a remark here: the post-condition is valid modulo the assumption > that the loop invariant is valid (if you have a look at the why gui, > you'll see an hypothesis corresponding to the invariant) and the loop > test is false (same thing). But this still leaves the issue of proving > that the loop invariant holds. > >> Is it possible we miss something in the specification? Maybe another loop invariant? >> It is possible to prove that \forall integer k; 0 <= k < size ==> a[k] == k; > > Not with your current loop invariant. Remember that when considering a > loop, the only thing that jessie knows of all the steps preceding the > current ones is the loop invariant. Conversely, everything which is not > stated in the loop invariant is out of reach. In order to complete the > proof, you'll thus have to add another invariant stating that: > loop invariant \forall integer k; 0<=k<i ==> a[k] == k; > (in fact, since this invariant implies that \forall k; 0<=k<i-1 ==> > a[k]<=a[k+1], the latter becomes useless as a loop invariant). > > Best regards, -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |