val N:ℕ;
val M:ℕ;

type elem = ℕ[M];
type array = Array[N,elem];
type int = ℤ[-1,N];

proc bsearch(a:array,x:elem,from:int,to:int):int 
{
  var r:int ≔ -1;
  var low:int ≔ from;
  var high:int ≔ to;
  while r = -1 ∧ low ≤ high do
  {
    val mid = (low+high)/2;
    if a[mid] = x then
      r ≔ mid; 
    else if a[mid] < x then 
      low ≔ mid+1;
    else 
      high ≔ mid-1;
  }
  return r;
}