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] lower_bound

  • Subject: [Frama-c-discuss] lower_bound
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Wed Nov 19 13:30:31 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