--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on November 2008 ---
Hi again, today I try to annotate a lower_bound algorithm: It returns a pointer to the first element in the sorted range [first,last) which does not compare less than value. The comparison is done using operator <. For the function to yield the expected result, the elements in the range shall already be ordered according to the same criterion (operator < ). The current state is: /*@ requires first <= last; requires \valid_range(first, 0, last-first-1); requires ascending_array(first, last-first); ensures \forall integer k; 0 <= k < \result-first ==> first[k] < value; behavior found: ensures value <= *\result; behavior not_found: ensures \result == last; */ int* lower_bound ( int* first, int* last, int value ) { int len = 0; len = last - first; //distance(first, last, len); int half; int* middle; int* it = first; /*@ loop invariant 0 <= it <= last-first; loop invariant \forall integer k; 0 <= k < it-first ==> first[k] < value; */ while (len > 0) { half = len >> 1; // half = len/2; middle = it; middle = middle + half; // advance(middle, half); if (*middle < value) { it = middle; ++it; len = len - half - 1; } else len = half; } return it; } This is a straight-forward attempt. Studying the binary_search example was not helpful. I want to know if there is a possibility to strengthen the loop invariant or is it impossible to prove it in the way I intended. Even if the question is far from accurate, I hope for help. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081119/1c5fd387/attachment.html