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>.

Solution

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

 Solution (source code)