Fixing The Program (Program Correctness)

• Mar 21st 2009, 12:58 PM
fusion1455
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 p:(ans=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
• Mar 21st 2009, 01:35 PM
Program correction
Hello fusion1455

I'm not quite sure what this means
Quote:

Originally Posted by fusion1455
... the loop invariant p:(ans=a1+...+ai) ^ (i <= n).

and I'm also not too sure how your pseudocode is usually set out, but in this code:
Quote:

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.

• Mar 21st 2009, 02:17 PM
CaptainBlack
Quote:

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.