--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on June 2009 ---
I think this is a pertinent question that would possibly help more people. 2009/6/24 Ulisses Ara?jo Costa <ulissesaraujocosta at gmail.com> > 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 tried to fix but failed. Can you help me? > > Cheers, > > -- > Ulisses Ara?jo Costa - http://caos.di.uminho.pt/~ulisses/<http://caos.di.uminho.pt/%7Eulisses/> > -- 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/20090626/c944125c/attachment.htm