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