{ n >= 0 and for all 0 <= j <= k < n : a[j] <= a[k] }
l = 0;
u = n - 1;
while (l < u)
i = (l + u - 1) / 2;
if (a[i] < x)
l = i + 1;
else
u = i;
{ 0 <= l < n and for all 0 <= j < l : a[j] < x and for all l <= j < n : a[j] >= x }