Binary Search


Algorithm description

This example was taken from the paper Discrete Loops And Worst Case Performance. The algorithm describes a binary search method using the divide-and-conquer strategy. Procedure binary_search has two inputs, arr (array of integers) and item (integer, which is searched for). The array is split into two disctinct subsets until item is found (in our example it is assumed that the searched item exists in the array).

Algorithm implementation

 1  function binary_search(item: integer; arr: sort_array) return index 
 2  is
 3      l : index := arr'first; -- first element of array
 4      u : index := arr'last; -- last element of array
 5      m : index; 
 6  begin
 7      discrete (l,u) -- two-dimensional identifier
 8          new (l,u) := (l,(l+u)/2-1) | ((l+u)/2+1,u) 
 9      with i := u-l+1 new i<=i/2 loop
10          m:=(l+u)/2; -- split array into subsets
11          if item < arr(m) then
12              u := (l+m-1)/2-1; -- compute new upper bound
13          elsif item > arr(m) then
14              l := (m+1+u)/2+1; -- compute new lower bound
15          else
16              return m; -- return index of found item
17          end if;
18          i := u-l+1; 
19      end loop;
20  end binary_search;

Notes on design

Since the present implementation of the preprocessor does not allow more than one identifier in the discrete-loop, our example is not executable at the moment. Due to the non-monotony of the binary search algorithm in general, we had to choose a discrete loop with a remainder function using another hidden monotonical sequence in the algorithm, namely the length of the intervals.

Worst Case Performance

Every time we compare 'item' with the borders of both subsets, we can dismiss half of our elements. Hence it follows that successful searching in an array of N elements never leads to more than

ceiling( ld(N+1) )

comparisons (and loop iterations).

Selected Bibliography

[AHU83, p. 366] [Hel86, p. 197] [Ott93, p. 185] [Sed88, p. 198]


[ Samples Overview | Bibliography | WOOP Project ]