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−1 
        * 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.