Reading material

Pages 140-142.

Additional material

Proof system: PostScript and PDF

Question

Add assertions to
{ 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 }