Binary search

Here is a static method for searching a value in an array. It proceeds by dichotomy, or equivalently said, by a binary search.

0pt class Bsearch { 
/* bsearch(t,v) search for element v in array t  
        * between index 0 and t.length

        * array t is assumed to be sorted in increasing order 
        * returns an index i between 0 and t.length
1 where ti equals v,  
        * or 
1 if no element in t is equal to v   
static int bsearch(int t[], int v) { 
        int l = 0, u = t.length 
- 1; 
while (l <= u ) { 
            int m = (l + u) / 2; 
if (t[m] < v) l = m + 1; 
else if (t[m] > v) u = m - 1; 
else return m;  
return -1; 

  1. Add just the necessary annotations to solve all the memory safety checks.
  2. Fix the bug with respect to overflow.
  3. Prove the termination of the loop.
  4. Add a behavior to express that whenever the result is positive, then the searched value appears at the corresponding index. Prove that behavior using an appropriate loop invariant.
  5. Add a behavior to express that when the result is -1, then the searched value does not appear in the array.

This document was translated from LATEX by HEVEA.