#include "arrays.pi"

define int ix = ?;

@pre  0 <= l && u < length(a) && sorted(a, 0, length(a) - 1)
@post rv <-> exists(ix, l, u, a[ix] == e)
bool BinarySearch(int[] a, int l, int u, int e)
declare
  int m;
{
  if (l > u) 
    return false;
  else {
    m = (l + u) div 2;
    if (a[m] == e) 
      return true;
    else if (a[m] < e) 
      return BinarySearch(a, m + 1, u, e);
    else 
      return BinarySearch(a, l, m - 1, e);
  }
}