Homework: Proofs of Program Correctness

Consider the following program fragment, with initial and final assertions added:

$\{n>0\}$

ans $=0$;

$k=0$;

$\{$ Invariant:

while $(k0$ and ans $=n\frac{n+1}{2}\}$

a$)$ Fill in the invariant assertion above.

b$)$ Prove that the loop terminates.

c$)$ Give a proof of partial correctness that this program produces its final assertion when started with the initial assertion holding true. Be very clear about each inference rule that you use.