Loop invariants and termination

Consider a sorted array of length n and a target t. We want its lower-bound index: the first position whose value is at least t, allowing n when every value is smaller. This specification handles missing values and duplicates without exceptional meanings. Maintain indices l and r with the unresolved positions in the half-open interval [l,r). Positions before l are known to be too small; positions from r onward are known to be large enough. The indices satisfy zero ≤ l ≤ r ≤ n.

Initially l is zero and r is n. Both known regions are empty, so their universal claims hold vacuously. When l is smaller than r, choose the midpoint m by rounding their average downward. If the value there is smaller than t, sortedness certifies that every position through m is too small, so set l to m plus one. Otherwise every position from m onward is large enough, so set r to m. Neither update discards an unresolved candidate without a reason.

Initialization proves the assertion before the first iteration. Preservation assumes it before an arbitrary iteration and derives it afterward. These steps are ordinary induction on the iteration number. At exit the guard l < r is false, while the invariant still gives l ≤ r, hence l equals r. The unresolved region is empty. Its shared boundary is exactly the first index that can satisfy the target comparison, including the legal answer n.

This establishes partial correctness: if the loop exits normally, the returned answer meets the specification. It does not establish that an exit occurs. The deliberately broken update l = m in the smaller-value branch preserves the classification but can stall when r = l + 1. An invariant that merely says the answer has not been discarded cannot detect that failure. Correctness arguments need both a description of the remaining candidates and an explicit explanation of progress.

A termination variant must take values in a well-founded order. Positive real values are insufficient: repeatedly halving one gives an infinite strictly decreasing sequence. Here integer interval lengths make the proof work. Each iteration takes constant time in a random-access comparison model with array entries and indices fitting machine words. The interval roughly halves, giving logarithmically many iterations. This resource bound is a separate theorem from correctness and should identify the operations being counted.

Implementation details can invalidate an otherwise sound proof. In a bounded integer type, adding l and r may overflow even when each index is valid. Computing l plus the integer half of r minus l avoids that sum under suitable nonnegative index bounds. Concurrent mutation can destroy sortedness during the search. An expensive comparison changes the time model. Writing assumptions beside the invariant makes these failure modes visible and tells a reviewer which parts belong to mathematics and which belong to the programming environment.