(1) Identify an invariant predicate of the while loop suitable for proving that the algorithm returns the expected value.

(1)

Identify an invariant predicate of the while loop suitable for proving that the algorithm returns the expected value. Then, give a loop variant expression suitable for proving that the algorithm will always terminate.

ALGORITHM SumPos(A[0..n - 1])

// Returns the sum of the positive numbers in an array A of length n. We

// assume that the sum of the numbers in an array of length zero is zero.

t ← 0

i ← 0

while i ≠ n do

if A[i] > 0

t ←t + A[i]

i ← i + 1

return t