partial vs total correctness

There are two different promises you might make about a program. The weaker one: 'IF it stops, the answer is right.' The stronger one: 'It stops, AND the answer is right.' The gap between them is the possibility that the program runs forever. Partial correctness covers only the first promise; total correctness adds the guarantee that the program actually halts. A program that loops forever is, oddly, partially correct (it never produces a wrong answer because it never produces any answer), but it is useless — which is why we usually want total correctness.

Precisely: given a precondition (what is assumed about the input) and a postcondition (what should be true of the output), partial correctness says 'whenever the precondition holds and the program terminates, the postcondition holds.' Total correctness says 'whenever the precondition holds, the program terminates and the postcondition holds.' The two proofs split cleanly: the loop-invariant / induction argument establishes partial correctness (the result is right at exit), and a separate well-founded termination measure establishes that an exit always happens. Together they give total correctness. So total correctness = partial correctness + termination.

Keeping these separate is practically important. Many correctness write-ups quietly prove only partial correctness and forget termination — fine for code you already know halts, dangerous for code that might not. Conversely, you can have termination without correctness (a program that always stops but stops with the wrong answer). In some settings (reactive systems, servers) you actually want non-termination, so 'total correctness' is reframed in terms of other properties. The clean takeaway: an invariant proves the answer is right when the loop ends; a measure proves the loop ends; you need both for the full guarantee.