--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2009 ---
Hello Claude, thanks for the pointer to the jessie tutorial. We were trying to prove the postcondition without "advanced algebraic modeling". The reason for this attempt is a customer that feels a bit overwhelmed by inductive definitions. Do you think it is possible that Jessie can prove a sort algorithm that has not been "inductively specified"? Regards Jens Am 03.06.2009 um 16:42 schrieb Claude March?: > > 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,