--- layout: fc_discuss_archives title: Message 106 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,

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