What does proving partial correctness of a page-draining loop leave unproven, and what closes that gap?

## Two claims, proved separately Correctness of a loop is conventionally split into two claims because they are proved by different means and fail in different ways. - **Partial correctness**: *if* the loop terminates, the final state satisfies the postcondition. Proved from the invariant's three obligations — initialization, maintenance, and the exit step that combines the invariant with the negated guard. - **Total correctness**: partial correctness **and** the loop terminates on every input the precondition allows. The extra ingredient is a measure argument. | | Partial correctness | Total correctness | |---|---|---| | Claim | If it halts, the answer is right | It halts, and the answer is right | | Proved from | The loop invariant | The invariant plus a decreasing measure | | A loop that spins forever | Satisfies it vacuously | Fails it | | Failure looks like | Wrong or incomplete output | A hang, or a job that never finishes | ## Why a non-terminating loop is "partially correct" This is the part that reads as a trick and is not. The exit obligation has the form *invariant and not-guard implies postcondition*. If the guard is never false, that implication is never exercised; an implication with a false antecedent is true. So a drain loop that refetches the same page forever is partially correct with respect to any postcondition you like. Nothing has been proved about it because nothing was claimed — that is the honest reading of "partial". The practical consequence: an invariant review that finds nothing wrong has not told you the job finishes. Those are separate reviews. ## What a termination argument looks like You exhibit a **measure**: an expression over the loop's own state, with two properties. 1. It **strictly decreases** on every pass — not on most passes, not on average. 2. It is **bounded below**, so it cannot decrease forever. In practice the measure is an integer with a floor, which is what an interviewer expects you to produce. For the drain loop the natural measure is the number of records still beyond the cursor. Each pass appends a page and moves the cursor past it, so if every page is non-empty the measure strictly falls and cannot go below zero — finitely many passes, done. The moment a page may be empty while the cursor stands still, the measure fails property 1 and the termination claim evaporates, even though the invariant is untouched. ## The two failure modes are not interchangeable - A **partial-correctness failure** is a wrong answer: the sink is missing records, or holds duplicates. It is visible in the output, and downstream systems may act on it. - A **termination failure** is a hang: the job holds its resources and never reports. The output is not wrong; there is no output. Engineers who only ever test tend to conflate them, because a test suite that passes shows both "right answers" and "finished in time" on the inputs tested. Neither generalises. Tests sample inputs; both proofs quantify over all of them. ## Where each claim is the one you want - Loops whose measure is internal — an index walking a fixed-size collection, a window shrinking toward empty — usually make total correctness easy, and there is no reason to settle for partial. - Loops whose measure depends on something outside your code — a source that decides when the data ends — can honestly be proved only partially correct on their own. Termination there is an assumption about the environment, and it is better stated as an assumption than quietly assumed. - **Termination is not performance.** A measure that starts enormous and falls by one per pass proves the loop stops; it says nothing about whether it stops soon enough. Running time is a different question with different tools. ## Saying it in an interview Name the split, then say which half you have. "The invariant gives me partial correctness — the sink is exactly the fetched records. For termination I need the count of unfetched records to strictly drop each pass, and that holds only if every page is non-empty, so that is the precondition I would state or enforce." That answer shows both obligations and the place the second one is fragile.