Use the loop invariant I to show that the code below correct

Use the loop invariant (I) to show that the code below correctly computes the product of all elements in an array A of n integers for any n greaterthanorequalto 1. First use induction to show that (I) is indeed a loop invariant, and then draw conclusions for the termination of the while loop. computeProduct(int[] A, int n) p = a[0] i = 0 while i

Solution

Case 1:

Consider i=0, so p = a[0] (given before the loop).

Case 2:

Assume it is true for I=q(<n-1). So p = a[0].a[1].a[2]....a[q]. In the next loop iteration i becomes q+1. Next statement is p = p*a[i]. Evaluation the Right Hand side:

p *a[i] => p*a[q+1] => a[0].a[1]...a[q].a[q+1]. This is assigned to p, sp p becomes a[0].a[1]...a[q].a[q+1] for i = q+1. Hence the invariant is still holding.

So by induction the given statement is a loop invariant.