# Thread: Fixing The Program (Program Correctness)

1. ## Fixing The Program (Program Correctness)

Consider the following buggy program to compute the sum of a sequence of integers a1,...,an with respect to the initial assertion n>=2 and the final assertion that ans = a1+...+1n. It was designed using the loop invariant pans=a1+...+ai) ^ (i <= n).

Modify the program so that p is truly a loop invariant and then prove it is correct.

Procedure sum({a1,...,an})
ans = a1 + a2

while i <= n - 1
ans = ans+ ai
i = i+1
return ans

2. ## Program correction

Hello fusion1455

I'm not quite sure what this means
Originally Posted by fusion1455
... the loop invariant pans=a1+...+ai) ^ (i <= n).
and I'm also not too sure how your pseudocode is usually set out, but in this code:
Procedure sum({a1,...,an})
ans = a1 + a2

while i <= n - 1
ans = ans+ ai
i = i+1
return ans
it seems to me that (a) you haven't initialised i to the value 3, and (b) you haven't indicated where the end of the while loop is.

Hello fusion1455

I'm not quite sure what this means
and I'm also not too sure how your pseudocode is usually set out, but in this code:it seems to me that (a) you haven't initialised i to the value 3, and (b) you haven't indicated where the end of the while loop is.