Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] loop invariant and side effects
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Wed, 28 Jan 2009 13:35:07 +0100
        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