--- layout: fc_discuss_archives title: Message 105 from Frama-C-discuss on June 2009 ---
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