(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