Chapter 5.5, Problem 8ES

Exercises 6-9 each contain a while loop annoted with a pre-and a post-condition and also a loop invariant. In each case, use the loop invarient theorem to prove the correctness of the loop with respect to the pre-and post-conditions.
8. [Pre-condition: $sum=A\left[1\right]$ and $i=1$ ] while $\left(i\ne m\right)$
1. $i:=i+1$
2. sum $:\text{sum}\text{+}A\left[i\right]$
End while
[Post-condition: $sum=A\left[1\right]+A\left[2\right]+\cdot \cdot \cdot +A\left[m\right]$] loop invariant: $l\left(n\right)$ is “ $i=n+1$ and $sum=A\left[1\right]+A\left[2\right]+\cdot \cdot \cdot +A\left[n+1\right]."$