Question

Multiple Choice:

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.

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

	A.	Q: j = a[1] + … + a[i – 1] Q(0): j0 = a[1] + … + a[i0 – 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): jk = a[1] + … + a[ik – 1] Q(k + 1): jk+1 = a[1] + … + a[ik+1 – 1]             note: jk+1 = jk + a[ik] and ik+1 = ik + 1             jk+1                                                    left side of Q(k + 1)             jk + a[ik]                                            assignment rule             a[1] + … + a[ik – 1] + a[ik]               inductive hyp             ik+1 = ik + 1 so ik = ik+1 - 1               rewrite             a[1] + … + a[ik – 1] + a[ik+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]
	B.	begins the sum with a[0]
	C.	makes one too many passes through the loop and adds a[n+1] to the sum
	D.	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
	E.	none of these are correct

Answer 1

A.

Q: j = a[1] + … + a[i – 1] Q(0): j0 = a[1] + … + a[i0 – 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): jk = a[1] + … + a[ik – 1] Q(k + 1): jk+1 = a[1] + … + a[ik+1 – 1]             note: jk+1 = jk + a[ik] and ik+1 = ik + 1             jk+1                                                    left side of Q(k + 1)             jk + a[ik]                                            assignment rule             a[1] + … + a[ik – 1] + a[ik]               inductive hyp             ik+1 = ik + 1 so ik = ik+1 - 1               rewrite             a[1] + … + a[ik – 1] + a[ik+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]