Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 1 / a

A loop invariant is a property of the program state that holds whenever control reaches the loop's condition, including the final failed test. Its main purpose is proving partial correctness: establish it initially, prove one guarded iteration preserves it, then combine it with the negated condition to obtain the postcondition. A separate loop variant or another progress argument proves algorithm termination and hence total correctness.