--- layout: fc_discuss_archives title: Message 106 from Frama-C-discuss on June 2009 ---
Hello, if someone can prove that, the problem is from my machine. In fact I don't have z3 instaled, and my simplify version is 1.5.4. I will try in other computer. Thank you, 2009/6/30 Virgile Prevosto <virgile.prevosto at cea.fr> > Hello, > > Le mer. 24 juin 2009 16:36:07 CEST, > Ulisses Ara?jo Costa <ulissesaraujocosta at gmail.com> a ?crit : > > > Hello everyone, > > > > apparently the example that the online manual has a problem with the > sorting > > algorithm. > > It seems that frama-c can not prove the preservation of the outer-loop > > invariant: > > > > @ Sorted(t,0,i) && > > @ (\forall integer k1, k2 ; > > @ 0 <= k1 < i <= k2 < n ==> t[k1] <= t[k2]) ; > > > > > I'm unsure of what you mean by 'frama-c can not prove ...' Both with > Lithium and Beryllium beta, all proof obligation for the min_sort > algorithm of Jessie's manual are discharged by the combination of > alt-ergo (v0.8), Simplify (v1.5.7) and Z3 (v2.0). 1 PO is discharged > only by alt-ergo, while 2 POs are discharged by Simplify and Z3, but not > alt-ergo, including one PO related to one of the loop invariant of the > outer loop of min_sort function. Is that the issue you're mentioning? > No prover can handle all POs alone, but this is a known fact. It is > better to work with two or more (I tend to rely on the three above, but > this is a matter of personal choice), if things go really wrong, with > coq, pvs or Isabelle. > > Best regards, > -- > E tutto per oggi, a la prossima volta. > Virgile > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Ulisses Ara?jo Costa - http://caos.di.uminho.pt/~ulisses/ -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090630/e245de0a/attachment.htm