Proving Termination and Partial Correctness of a Boundary-Search Loop

Welcome back. You now have the core ingredients of a robust boundary search: a monotone predicate, a half-open interval contract, invariant-preserving updates, and an overflow-safe lower midpoint. This lesson puts them together into the proof that makes the template trustworthy.

We will prove two claims about a first-true search:

1. Partial correctness: if the loop finishes, its returned value satisfies the boundary contract.
2. Termination: the loop must finish on every finite, representable search interval.

Together, these give total correctness.

---

1. Start with a precise contract

Consider this C++20 first-true template:

#include <numeric>

template <class Pred>
int first_true(int lo, int hi, Pred P) {
    while (lo < hi) {
        int mid = std::midpoint(lo, hi);

        if (P(mid)) {
            hi = mid;
        } else {
            lo = mid + 1;
        }
    }
    return lo;
}

Let the original input interval be $[a,b)$, where initially:

lo = a;
hi = b;

Assume:

• The interval is finite and its endpoints are representable as int.
• P is deterministic: evaluating it twice at the same input gives the same result.
• P is monotone nondecreasing over the domain:

$$i < j \land P(i) \implies P(j)$$

In other words, once P becomes true, it stays true as the input increases.

The desired postcondition for the returned value $q$ is:

$$a \le q \le b$$ $$\forall x \in [a,q), \neg P(x)$$ $$\forall x \in [q,b), P(x)$$

This contract deliberately handles every edge case:

Predicate pattern on $[a,b)$	Returned $q$
All values are false	$b$
All values are true	$a$
False values followed by true values	First true position

Notice an important detail: when $q=b$, we do not evaluate P(b). It is a past-the-end boundary, not necessarily a valid predicate input.

The resource below presents the same idea using explicit false and true sentinels around the searchable indices. Its proof sketch is compact, but its sentinel-style loop is not identical to the half-open loop we will prove here.

{"type":"reading","par_intro":"Read the “Search on arbitrary predicate” section from Algorithms for Competitive Programming. It gives a concise invariant-based proof of locating a false-to-true transition.","par_directions":"In “Search on arbitrary predicate,” first read the paragraph defining a monotonically increasing Boolean function. Then read the <span data-type=\"resource_reading_textrange\" data-resource-subitem-id=\"1236d6d0\" data-range-start=\"Proof of correctness supposing a transition point exists, that is\" data-range-end=\"giving us our desired transition point.\">proof sketch</span>. Focus on the two proof ingredients: preserving known false and true positions, and showing that the remaining gap shrinks. Their code uses external sentinels; keep that invariant separate from the half-open invariant developed below.","learning_duration":"8 minutes","url":"https://cp-algorithms.com/num_methods/binary_search.html","title":"Binary Search - Algorithms for Competitive Programming","isV2":true,"blockId":"5430a919-ce8d-44e3-9e1c-ddf16d5a5c94","lessonId":"bc600820-9e19-4ce8-a195-ea5c9f28086c"}

{
  "type": "exercise",
  "id": "1412e30e-11e2-4068-9cc4-3fc010a73150"
}

---

2. The loop invariant: turn the final contract into a live claim

A loop invariant is a statement that is true before the first iteration and remains true after every completed iteration.

For first-true search, use this invariant:

$$a \le \texttt{lo} \le \texttt{hi} \le b$$ $$\forall x \in [a,\texttt{lo}), \neg P(x)$$ $$\forall x \in [\texttt{hi},b), P(x)$$

Read it operationally:

• Everything strictly left of lo has been proved false.
• Everything at or right of hi has been proved true.
• Only $[\texttt{lo},\texttt{hi})$ remains unresolved.

This is stronger and more useful than merely saying “the answer is still somewhere in the interval.” It records why discarded positions cannot contain the first true value.

Initialization

Before the loop:

lo = a;
hi = b;

The bounds condition holds immediately:

$$a \le a \le b \le b$$

The two logical regions are empty:

$$[a,\texttt{lo}) = [a,a)$$ $$[\texttt{hi},b) = [b,b)$$

A universal statement about an empty set is true. There are no positions left of a that need to be false, and no positions at or beyond b that need to be true. Therefore, the invariant holds before the first iteration.

This is one reason half-open intervals are so clean: initialization needs no special case for an empty domain.

---

3. Maintenance: why each update preserves the invariant

Assume the invariant holds at the start of an iteration and the guard is true:

$$\texttt{lo} < \texttt{hi}$$

Because std::midpoint(lo, hi) returns the lower midpoint for ordered integer arguments:

$$\texttt{lo} \le \texttt{mid} < \texttt{hi}$$

Thus, mid is always a valid, unresolved position in the active interval.

There are two cases.

Case 1: P(mid) is true

The code executes:

hi = mid;

The new known-true region is $[\texttt{mid},b)$.

Why is every value in that region true?

• P(mid) is true by the branch condition.
• By monotonicity, every position greater than mid is also true.
• The previously known-true region $[\texttt{hi},b)$ remains true as well.

So after setting hi = mid:

$$\forall x \in [\texttt{hi},b), P(x)$$

The known-false region has not changed because lo did not change.

The bounds remain valid because:

$$\texttt{lo} \le \texttt{mid} < \texttt{hi} \le b$$

So the invariant is preserved.

Case 2: P(mid) is false

The code executes:

lo = mid + 1;

The new known-false region is $[a,\texttt{mid}+1)$.

Why is every value there false?

• P(mid) is false by the branch condition.
• If some $x \le \texttt{mid}$ were true, monotonicity would force P(mid) to be true too. That contradicts the branch condition.
• Therefore, every value at or left of mid is false.

After assigning lo = mid + 1:

$$\forall x \in [a,\texttt{lo}), \neg P(x)$$

The known-true region does not change because hi does not change.

The bounds remain valid because:

$$\texttt{lo}_{\text{old}} \le \texttt{mid} < \texttt{hi}$$

so:

$$\texttt{mid} + 1 \le \texttt{hi}$$

Thus the invariant is preserved in this branch too.

A concrete trace

Take:

$$P(x) \equiv x^2 \ge 30$$

over $[0,10)$. The first true value is $6$.

lo	hi	mid	P(mid)	Resulting unresolved interval
0	10	5	false	$[6,10)$
6	10	8	true	$[6,8)$
6	8	7	true	$[6,7)$
6	7	6	true	$[6,6)$

At every stage, the values left of lo are known false, values at or right of hi are known true, and only the displayed interval is undecided.

---

4. Termination: prove a quantity strictly decreases

Preserving the invariant is not enough. A loop could preserve an invariant forever.

For termination, define the variant:

$$V = \texttt{hi} - \texttt{lo}$$

The bounds part of the invariant gives:

$$V \in \{0,1,2,\ldots\}$$

So $V$ is always a nonnegative integer.

Whenever the loop runs, lo < hi, hence $V>0$. We now show that each branch strictly decreases $V$.

True branch

When P(mid) is true:

hi = mid;

The new variant is:

$$V' = \texttt{mid} - \texttt{lo}$$

Since:

$$\texttt{mid} < \texttt{hi}$$

we get:

$$V' < \texttt{hi} - \texttt{lo} = V$$

False branch

When P(mid) is false:

lo = mid + 1;

The new variant is:

$$V' = \texttt{hi} - (\texttt{mid}+1)$$

Since:

$$\texttt{lo} \le \texttt{mid}$$

we have:

$$\texttt{lo} < \texttt{mid}+1$$

Therefore:

$$V' < \texttt{hi} - \texttt{lo} = V$$

In both branches, $V$ remains a nonnegative integer and strictly decreases. A nonnegative integer cannot decrease forever. By the well-ordering principle, eventually $V=0$, meaning:

$$\texttt{lo} = \texttt{hi}$$

At that point the loop condition is false, so the loop terminates.

The short video segment below emphasizes the key implementation fact behind this argument: the midpoint is strictly below high when the active interval is nonempty.

{"type":"video","title":"Binary Search - A Different Perspective | Python Algorithms","learning_duration":52,"video_id":"tgVSkMA8joQ","par_intro":"Watch “Binary Search - A Different Perspective” by mCoding for a compact explanation of why the distance between the bounds shrinks on every iteration.","par_directions":"In the segment beginning just after the implementation, watch <span data-type=\"resource_video_timerange\" data-resource-subitem-id=\"09207df8\" data-range-start=\"361\" data-range-end=\"413\">the termination argument</span>. Focus on the justification that the midpoint is strictly less than the upper bound, which makes the `hi = mid` branch progress rather than stall.","video_duration":536,"isV2":true,"blockId":"848bf77b-2a34-471a-a4bf-341a9023c359","lessonId":"bc600820-9e19-4ce8-a195-ea5c9f28086c"}

{
  "type": "exercise",
  "id": "40b83f33-f110-4131-979f-ebccbc56cc52"
}

---

5. Partial correctness at loop exit

Now suppose the loop has ended.

The loop guard is false, so:

$$\neg(\texttt{lo} < \texttt{hi})$$

The bounds invariant also says:

$$\texttt{lo} \le \texttt{hi}$$

The only possibility is:

$$\texttt{lo} = \texttt{hi} = q$$

The function returns lo, so it returns $q$.

Substitute $q$ for both bounds in the invariant:

$$\forall x \in [a,q), \neg P(x)$$ $$\forall x \in [q,b), P(x)$$

Those are exactly the desired postconditions.

There are two interpretations:

• If $q<b$, then P(q) is true and every earlier position is false. Thus $q$ is the first true value.
• If $q=b$, every position in $[a,b)$ is false. Thus no true value exists in the original domain, and returning the past-the-end boundary is correct.

So the function is partially correct. Since the preceding variant proof established termination, the function is totally correct.

{
  "type": "exercise",
  "id": "eb76e651-fb0d-4edd-bb51-bbb7ea6c21f8"
}

---

6. A proof-writing template for interviews and contests

For a boundary-search explanation, avoid saying only “binary search cuts the range in half.” That is intuition, not a proof. A compact rigorous explanation has four parts:

1. Contract
   State exactly what the result means, including all-false and all-true cases.

2. Invariant
   State the bounds and what has been established outside the active interval.

3. Maintenance
   For each branch, explain:

   • what new region has become known;
   • where monotonicity is used;
   • why the new bounds remain valid.

4. Termination and exit
   Use an integer variant such as hi - lo, prove strict decrease, then apply the invariant once lo == hi.

For a short proof, this is usually sufficient:

Maintain that every value before lo is false and every value from hi onward is true. At a midpoint, a true result makes the suffix beginning at mid true by monotonicity, so set hi = mid; a false result makes the prefix through mid false, so set lo = mid + 1. The width hi - lo is a nonnegative integer and decreases strictly in either branch. When the bounds meet, the invariant states exactly that the meeting point is the first true position, or the end if no true position exists.

Focused practice protocol

Spend about 10 minutes writing this proof without looking at the template:

• Write the three invariant clauses first.
• For each branch, name the exact newly eliminated interval.
• State precisely where monotonicity is used.
• Finish with the variant $V=\texttt{hi}-\texttt{lo}$, not an informal claim that the range “roughly halves.”
• At exit, substitute lo == hi into the invariant and derive the return contract.

If any sentence says only “we discard this half,” strengthen it by stating what predicate value has been proved for that discarded region.

---

Conclusion

A correct boundary search rests on two complementary arguments:

• The loop invariant proves that discarded positions are classified correctly: false on the left and true on the right.
• The variant $\texttt{hi} - \texttt{lo}$ proves that the active interval cannot remain nonempty forever.

At termination, lo and hi meet at exactly the boundary promised by the contract. This is why the familiar updates hi = mid and lo = mid + 1 are not arbitrary off-by-one conventions: each is forced by the invariant and the requirement of strict progress.

Next, you will turn this proof-backed idea into reusable C++ boundary-search templates, beginning with a callable half-open first_true implementation.