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