Total correctness
= Total correctness
<Total correctness> requires <partial correctness> and <algorithm termination> for every <program state> allowed by the <precondition>. For a deterministic sequential program, every permitted start must reach a final <program state> satisfying the <postcondition> after finitely many steps. Thus an infinite execution can satisfy <partial correctness>, but refutes <total correctness> for a permitted start.
In the <summation loop verification>, the <loop invariant> establishes the answer conditional on exit, and the <loop variant> establishes exit. Both parts matter: replacing the body by a step that never returns would defeat <total correctness> even if every completed iteration preserved the <loop invariant>. Likewise, a terminating loop with the wrong <sum> fails <partial correctness> and therefore fails <total correctness>.
These obligations depend on the <formal specification>. A program that rejects every <input> might correctly implement a rejection service, but does not meet a contract promising a <sum> for every nonnegative <integer>. A proof of <total correctness> also gives no particular physical response-time guarantee: <time complexity> and the execution environment require their own assumptions.