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

[Frama-c-discuss] Selection Sort loop-invariant problem



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