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

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.

Grandad

Quote:

---

Originally Posted by Grandad

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.

Grandad

---

It is also not known what value n takes.

Presumably {a1, ... , an} denotes an arbitary list, but it still seems ill defined, something like:

Procedure sum(a[],n)

would be better, and referenced as a[i] , depending on the natrue of the psuedo-code you are using.

CB