Why can a loop invariant that genuinely holds on every pass still fail to prove the loop's result at exit?

## Two ways an invariant fails, and only one of them is being false When an invariant does not do its job, the instinct is to look for a pass that falsifies it. Often there is none: the claim is impeccably true every time round and still proves nothing. That is a **too-weak invariant**, and it fails the third obligation rather than the first two. Recall the exit obligation: *invariant AND not-guard IMPLIES postcondition*. The invariant is one of two premises in an implication. A premise can be true and irrelevant. ## Examples of true-but-useless For a loop draining pages into a sink, with postcondition "the sink holds every record the source yields, in order": - "`sink` is a list of records" — true throughout, says nothing about which records. - "the number of records in `sink` is at least zero" — true throughout, and arithmetic guarantees it whatever the body does. - "`cursor` holds a valid position or the exhausted marker" — a type-shaped claim; it survives a body that refetches page one forever. - "every record in `sink` came from some page" — closer, and still compatible with duplicates and with pages silently skipped. Each passes initialization and maintenance. None combines with "the cursor is exhausted" to yield the postcondition. ## What makes an invariant strong enough | Test | Weak invariant | Strong enough | |---|---|---| | Does it mention every object in the postcondition? | Mentions only the sink | Mentions the sink, the cursor and the relation between them | | Does it say what is *left* to do? | Silent | "the cursor marks the first record not yet fetched" | | Does the negated guard finish the argument? | No extra information is unlocked | Exhausted cursor plus the invariant gives "every record" | | Could a wrong body still satisfy it? | Yes — skipping or duplicating pages | No — exactness rules both out | The practical recipe is three steps. 1. Write the postcondition first, and underline every object it names. 2. Write a claim that mentions all of them and partitions the work into done and remaining. 3. Assume the guard is false and try to derive the postcondition on paper. If you cannot, the invariant is still too weak — and the derivation will usually show which missing clause would close it. ## Strengthening can also rescue maintenance There is a second, more surprising reason to strengthen. Sometimes maintenance itself will not go through, because at the top of the next pass you need to know something the invariant never claimed. Strengthening gives you a stronger hypothesis to assume as well as a stronger conclusion to prove, and the extra assumption can be worth more than the extra obligation. For a search loop, "the target is somewhere in the window" is too weak to survive an absent key; "if the target is present it is in the window, and everything outside is ruled out by the ordering" survives, and it is exactly the extra clause about what lies outside that makes the next discard justifiable. The balance point is real. Strengthen too far and the invariant becomes a restatement of the whole computation — impossible to keep true through the body and useless as a review artefact. The target is the weakest claim from which the postcondition still follows. ## The other side: when the invariant is not the problem A loop can also be fine on all three obligations and still misbehave, because the failure is termination rather than correctness — the search window that stops shrinking is the standard illustration. Before strengthening anything, decide which symptom you have: a wrong or incomplete result points at the invariant, a hang points at the measure. Strengthening an invariant will never fix a hang, and no amount of measure work will fill a sink that was missing pages. ## Signals in review - The invariant would still be true if the body were deleted. That is a type assertion, not an invariant. - It names none of the objects in the postcondition, or only one of them. - It talks exclusively about counters or indices and never about content. - Nobody can say, in a sentence, what the failed guard adds. - It holds just as well for a plausible wrong implementation — the sharpest test of the four, and the quickest to apply.