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.
ans = a1 + a2
while i <= n - 1
ans = ans+ ai
i = i+1