--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on June 2009 ---
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/ -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090624/f25f565d/attachment.htm