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



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