$3.$ Parts $($a$)$ and $($b$)$ refer to the following program.

$1.//$pre: M $>=0$

$2.$ j$0$

$3.$ S$0$

$4.//$LoopInv:

$5.$ while$($j $<$ M$)$:

$6.$ S$$S $+(3*$j$*$j$)+5$

$7.$ j$$j $+1$

$8.//$post: S $==(1/2)*((2*$M$*$M$*$M$)-(3*$M$*$M$)+(11*$M$))$

$($a$)[5$ marks$]$ State and prove a loop invariant for this program. Hint: the variable S is

named for $$sum$.$ You will need to find a relationship between S and j that holds at

every check of the loop condition.

$($b$)[3$ marks$]$ Using the fact that your proposed statement in part $($a$)$ is a loop invariant,

prove that this program has the partial correctness property. Your proof of partial cor$-$

rectness must not refer to any lines of code except for lines $4$ and $5.$