Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 4 / a

For a proposed loop invariant $I$, initial condition $P$, guard $B$, body $S$, and postcondition $Q$, establish these Hoare logic obligations:The first establishes $I$ before the loop; the second preserves it after each iteration; the third derives the desired result when the guard is false. Together they prove partial correctness. For total correctness, also prove algorithm termination, for example by a nonnegative integer loop variant that strictly decreases whenever the body executes. The loop invariant need not be the postcondition: it generally describes completed and unfinished work together.