--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on January 2009 ---
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