Wiki Agenda Contact Version française

Binary search in C annotated in ACSL

This is a C version of Binary Search, annotated in ACSL.

Authors: Claude Marché / Jean-Christophe Filliâtre

Topics: Arithmetic Overflow / Searching Algorithms / Tricky termination

Tools: Frama-C / Jessie

References: The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)

Here is the annotated source code 
/*@ predicate sorted{L}(long *t, integer a, integer b) =
  @    \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j];
  @*/

/*@ requires n >= 0 && \valid_range(t,0,n-1);
  @ ensures -1 <= \result < n;
  @ behavior success:
  @   ensures \result >= 0 ==> t[\result] == v;
  @ behavior failure:
  @   assumes sorted(t,0,n-1);
  @   ensures \result == -1 ==>
  @     \forall integer k; 0 <= k < n ==> t[k] != v;
  @*/
int binary_search(long t[], int n, long v) {
  int l = 0, u = n-1;
  /*@ loop invariant
    @   0 <= l && u <= n-1;
    @ for failure:
    @   loop invariant
    @   \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;
    @ loop variant u-l;
    @*/
  while (l <= u ) {
    int m = (l + u) / 2;
    //@ assert l <= m <= u;
    if (t[m] < v) l = m + 1;
    else if (t[m] > v) u = m - 1;
    else return m;
  }
  return -1;
}

The program above is the classical binary search for a given element in an array sorted in increasing order.

This program exposes a long-standing bug, that is the computation of l+u may overflow. When attempting to prove this program with Frama-C/Jessie, the VC corresponding to this overflow cannot be proved.

See also