Version simplifiée de la procédure de fouille binaire
-----------------------------------------------------

Version simplifiée pour l'analyse asymptotique.


  procedure binsearch( int n, 
                       keytype S[*], 
                       keytype x, 
                       res int location )
  # PRECONDITION
  #   n >= 0,
  #   ALL( 1 <= i < n :: S[i] <= S[i+1] ),
  #   SOME( k: nat :: 2^k = n )
  # POSTCONDITION
  #   SOME( 1 <= i <= n :: S[i] = x ) 
  #     => (1 <= location <= n) & S[location] = x,
  #   ALL ( 1 <= i <= n :: S[i] ~= x ) 
  #     => location = 0
  {
    int l = 1;
    int h = n;
    location = 0;
    while( l < h ) {
      int mid = (l + h) / 2;
      if ( x <= S[mid] ) {
        h = mid;
      } else { # x > S[mid]
        l = mid+1;
      }
    }
    if ( S[l] == x ) {
      location = l;
    }
  }