Consider the following program specification and implementation for determining the sum

of the of the first $m$ positive integers:

it$\_$sum $(m)$ where minN

$(1)jm$

$(2)s0$

$(3)$ while $j>0$ do

$(4)ss+j$

$(5),jj-1$

$(6)$ end

$(7)$ return $s$

$\{$output is $1+2+$dots$+m$ for positive $m$ and $0$ for $m=0$

$($a$)$ Use induction on the number of iterations of the while loop to prove that

$s=(j+1)+$dots$+m={\displaystyle \underset{i=j+1}{\overset{m}{}}}i,$ and $,j0$

are loop invariants $($sum is $0$ if there is no terms in the sum$).$

$($b$)$ Prove partial correctness. Probably it is good idea to do case $m=0$ separately.

$($c$)$ Prove termination of the program.