Mathematical Logic Algorithm

I need to write an algorithm with appropriate assertions and input and output specifications that gives the sum of n given numbers. Then I need to prove it. This is what I have, is it right?

Input:$\displaystyle n_{1},n_{2},...,n_{m}$

Output: $\displaystyle s$

Algorithm SUM

$\displaystyle \{n_{1},n_{2},...,n_{m} $ integers$\displaystyle , -\infty < n_{1},...,n_{m} < \infty \}$

$\displaystyle s \leftarrow 0; i \leftarrow 0$

Loop Invariant: $\displaystyle \{s=s+n_{i}, i=1,2,...,m \}$

Repeat until: $\displaystyle i=m$

$\displaystyle s \leftarrow s + n_{i}$

$\displaystyle i \leftarrow i + 1$

End repeat

Loop termination condition: $\displaystyle \{s=s+n_{i} \wedge i=m \}$

Output specification: $\displaystyle \{s= n_{1},n_{2},...,n_{m}\}$