--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie sort specification



Hello,

I've got a question regarding the specification of a very simplified piece of code, which actually started as a test for proving another more complex sorting algorithm.
In Jessie different provers we used do not prove that the values in the array are growing. There's always a problem with the loop invariants. The post conditions are valid.
Is it possible we miss something in the specification? Maybe another loop invariant?
It is possible to prove that \forall integer k; 0 <= k < size ==> a[k] ==  k;
Does someone know the reason why if this is valid we can't conclude ==> a[k] <= a[k+1]  ?

Very thankful for your advices,
Regards,

Kerstin

/*@
  requires size >= 0;
  requires \valid_range(a, 0, size-1);
  ensures \forall integer i ;
     0 <= i < size - 1 ==> a[i] <= a[i+1];
*/
void wrong_sort(int* a, int size)
{
    int i = 0;
    /*@
        loop invariant 0 <= i <= size;
        loop invariant \forall integer k; 0 <= k < i-1 ==> a[k] <= a[k+1];
    */
    for(i = 0; i < size; i++)
        a[i] = i;
}