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

[Frama-c-discuss] loop invariant and side effects



        Hello,

I am exploring the problems with loop invariants and expressions with side effects such as 

while(++i != ...).

I would like to know, what has to be modified in the following algorithm:

/*@

    requires 0 <= length;

    requires \valid_range(a, 0, length-1);

    assigns \nothing;

    ensures 0 <= \result <= length;

    ensures \forall int i; 0 <= i < length ==> a[i] <= a[\result];

    ensures \result != length <==> \exists int i; 0 <= i < length && a[i] == a[\result];


*/

int max_element_array (int* a, int length )

{

    int i = 0;

    int largest = i;

    if (i == length) return length;

    /*@

        loop invariant 0 <= i < length;

        loop invariant 0 <= largest < length;


        loop invariant \forall integer k; 

            0 <= k < i ==> a[k] <= a[largest];

    */

    while (++i != length ){

        if (a[largest] < a[i])

            largest = i;

    }

    return largest;

}

If I rewite the loop and the annotation in a way, that i is iterated befor the loop and after each iteration, the proof is no problem.

But with the nested incrementation I cannot preserve the loop invariant.



Cheers,

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090128/3dfe4c14/attachment.htm