Assume you are given the contract . Use correctness by construction (see slides for Lecture 3) to derive stepwise an algorithm with a while loop, picking as loop invariant .
Show every step of your derivation (indicating which Hoare logic rule you apply), starting from a trivial tableau and ending with a fully implemented program and its proof tableau. Show also the final program without the assertions.
Can't change a rubric once you've started using it.