The following function is intended to return the value of a1

The following function is intended to return the value of a[1] + a[2] + … + a[n] for n 1.
(The sum of the first n entries in an array of integers).
Prove that the function is correct, or explain why it does not produce correct results.

ArraySumC(integers n, a[1], a[2], … , a[n])
Local variables:
integers i, j
    i = 0
    j = 0
    while i n do
        j = j + a[i]
        i = i + 1
    end while
    // j now has the value of a[1] + a[2] + … + a[n]
    return j
end function ArraySumC

Multiple Choice Answers:

begins the sum with a[0]

none of these are correct

makes one too many passes through the loop and adds a[n+1] to the sum

Q: j = a[1] + … + a[i – 1]
Q(0): j₀ = a[1] + … + a[i₀ – 1]
            true since j = 0, i = 1 before the loop is entered, so the equation becomes
            0 = a[1-1] which is 0 = a[0] and there is no a[0] term so the value is vacuously 0.
Q(k): j_k = a[1] + … + a[i_k – 1]
Q(k + 1): j_k+1 = a[1] + … + a[i_k+1 – 1]
            note: j_k+1 = j_k + a[i_k] and i_k+1 = i_k + 1
            j_k+1                                                    left side of Q(k + 1)
            j_k + a[i_k]                                            assignment rule
            a[1] + … + a[i_k – 1] + a[i_k]               inductive hyp
            i_k+1 = i_k + 1 so i_k = i_k+1 - 1               rewrite
            a[1] + … + a[i_k – 1] + a[i_k+1 - 1]       by substitution
This is the right side of Q(k + 1) so Q is our loop invariant
At loop termination j = a[1] + … + a[i- 1] and i = n + 1, so j = a[1] + … + a[n]

Q: j = a[1] + … + a[n – 1]

Q(0): j0 = a[1] + … + a[n – 1]

           cannot be proven true for base case so the function is proven incorrect

Solution

Here is the code explained where it fails:

ArraySumC(integers n, a[1], a[2], … , a[n])
Local variables:
integers i, j
i = 0
j = 0
while i n do   //This loop runs for values from i = 0 to n. Note: This is running till n, and not n-1, and this starts from 0, and not 1.
j = j + a[i] //When i value is 0, it is reading value from a[0], but the input starts from a[1].
           //There is no value at index a[0].
i = i + 1
end while
// j now has the value of a[1] + a[2] + … + a[n]
return j
end function ArraySumC

So, the option is: a. begins the sum with a[0]