## § Correctness of binary search

#### § Closed-closed intervals

```
int binsearch(int l, int r, int val, int *xs) {
if (l == r) { return l; }
int mid = (l+r)/2;
if (xs[mid] <= val) {
return binsearch(l, mid, val, xs);
} else {
return binsearch(mid+1, r, val, xs);
}
}
```

We have `(l <= mid < r)`

since floor division of the form `(l+r)/2`

will pull values "downward". The length of the interval `[l, mid]`

is smaller
than the interval `[l, r]`

as `mid < r`

. The length of the interval
`[mid+1, r]`

is smaller than the interval `[l, r]`

as `l < mid+1`

. We
are monotonically decreasing on the quantity "length of interval", and terminate
the recursion when the length is zero.
#### § Closed-open intervals

```
int binsearch(int l, int r, int val, int *xs) {
if (r == l + 1) { return l; }
int mid = (l+r)/2;
if (xs[mid] <= val) {
return binsearch(l, mid, val, xs);
} else {
return binsearch(mid, r, val, xs);
}
}
```

We have `(l <= mid < r)`

since floor division of the form `(l+r)/2`

will pull values "downward". Furthermore, if `r = l + 1`

we end the
recursion. Thus, we are guaranteed that we will have that `r >= l + 2`

.
Hence, `mid = (l+r)/2 >= (l + l + 2)/2 >= l + 1`

. Thus, we have that:
`l`

is to the left of `mid=l+1`

is to the left of `r>=l+2`

. So the
intervals `[l, mid)`

and `[mid, r)`

will be smaller, as we cleanly "separate"
out `l`

, `mid`

, and `r`

.