--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] lower_bound



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