Homework 3

Assume you are given the contract $(x=x_0\wedge <!--\; \wedge \; -->x\ge <!--\; \ge \; -->0,y=x_0!)$. Use correctness by construction (see slides for Lecture 3) to derive stepwise an algorithm with a while loop, picking as loop invariant $y\ast <!--\; \ast \; -->x!=x_0!\wedge <!--\; \wedge \; -->x\ge <!--\; \ge \; -->0$ .

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.