Search=proc [t:type] (a:array[t],x:t) returns (i:int)
   requires 
      t has operations         
      lt,equal:proctype (t,t) returns (bool)
      such that t is totally ordered by lt, 
      and a is sorted in ascending order based in lt
   effects 
      If x is in a, returns i such that a[i]=x
      otherwise returns high(a)+1

Search=proc [t:type] (a:array[t],x:t) returns (int)
       where t has lt,equal:proctype (t,t) returns (bool)
  % logaritmikus keres‚s
  at=array[t]
  low:int := at$low(a)
  high:int := at$high(a)
  while (low<=high) do
    mid:int := (low+high)/2
    val:t := a[mid]
    if x<val then high:=mid-1
             elseif x=val then return (mid)
             else low:=mid+1
    end
  end
  return (at$high(a)+1)
end Search