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

[Frama-c-discuss] Problem with solver



Hello again,

I would like to post a question regarding the reverse algorithm I sent before.

Following combination of functions:

/*@
 requires \valid(a);
 requires \valid(b);
 ensures *a == \old(*b);
 ensures *b == \old(*a);
*/
void swap (int* a, int* b )
{
    int c = *a;
    *a = *b;
    *b = c;
}

/*@
 requires 0 <= length;
 requires \valid_range (a, 0, length-1);

 ensures \forall integer k; 0 <= k < length ==> \old(a[k]) == a[length-1-k];
 ensures \forall integer k; 0 <= k < length ==> a[k] == \old(a[length-1-k]);
*/
void reverse_array (int* a, int length)
{
    int index_a = 0;
    int index_backwards = length;
    
    /*@
     loop invariant 0  <= index_a <= index_backwards <= length;
     
     loop invariant index_a == length - index_backwards;
     
     
     loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == a[length-1-k];
     loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == \at(a[length-1-k],Pre);
    */
    while ((index_a != index_backwards) && (index_a != index_backwards-1))
    {
    index_backwards--;
        swap(&a[index_a], &a[index_backwards]);
        index_a++;
    }
}

My problem is the preservation of the rather complex loop invariant.
I do not understand what the problem might be and I would appreciate any helpful hint.


Cheers Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090108/28d426a2/attachment.htm