COMP 401, Spring 2008401-22a.1COMP 401, Spring 2008Answers to exercises for Chapter 3Loop invariant exercisesEach of the following segments of code performs some reasonable task. For each loop, find • a. the loop invariant, and • b. an appropriate post condition at the point indicated. Note: The loop invariant most commonly characterizes (using the loop index) how much of the loop's task has been accomplished. It often also states that the loop index falls within a specified range. Recall that all you know after a loop has finished is the conjunction (the and of) the invariant and the loop exit condition. A postcondition is often weaker than this conjunction; for example, you often don't care about the current value of the loop index variable.In each of the following code segments, the array b is an integer array indexed from 0 to 100. All variables other than b are integer variables; all variables have been initialized.Examples are included to help you get started. In the example and in the key (to be handed out later), an informal characterization of the formal description has been given; these are preceded by a double exclamation mark ('//!!'). You are encouraged to write such comments in the same format. In the problems, space has been left in the code for you to write the invariants and postconditions. Example 1:while (true) loop form.// precondition trueint i = 0;while (true){b[i] = 0;// inv: 0 <= i <= 100 and (Ar: 0 <= r <= i: b[r] == 0)//!! All entries in b[0..i] are equal to 0.if (i==100) break;i = i+1;}// loop post: (Ar: 0 <= r <= 100: b[r] == 0) //!! All entries in b[0..100] are equal to 0.Nonterminating for loop form.// precondition truefor ( int i=0; ; i++ ){b[i] = 0;// inv: 0 <= i <= 100 and (Ar: 0 <= r <= i: b[r] == 0)//!! All entries in b[0..i] are equal to 0.if (i==100) break;}// loop post: (Ar: 0 <= r <= 100: b[r] == 0) //!! All entries in b[0..100] are equal to 0.401-22a.2(Note that we could add "&& i == 100" to the loop postcondition for the first loop (but not the second),but we assume that is not of interest.)In the form, the range predicate (0 <= i <= 100) is not really required in the invariant, because the loop postcondition is implied by the conjunction of the remainder of the invariant (Ar: 1 <= r <= i: b[r]== 0) and the exit condition i = 100. We have included the range condition only because it is often required, and it does no harm except to complicate the invariant slightly.401-22a.3Problem 1.while(true) loop form.// precondition trueint i = 0;while (true){b[i] = i;// inv:: 0 <= i <= 100 and (Ar: 0 <= r <= i: b[r] = r)//!! Each entry in b[0..i] is equal to its index.if (i == 100) break;i = i+1;}// loop post: (Ar: 0 <= r <= 100: b[r] = r)//!! Each entry in b[0..100] is equal to its index. The range //!! condition is not required.Nonterminating for loop form.// precondition truefor (int i=0; ; i++){b[i] = i;// inv:(Ar: 1 <= r <= i: b[r] = r)//!! Each entry in b[1..i] is equal to its index.if (i == 100) break;}// loop post: (Ar: 1 <= r <= 100: b[r] = r)//!! Each entry in b[0..100] is equal to its index.Example 2. while(true) loop form.// precondition lo <= hiint maxval = b[lo];int i = lo + 1;while (true){// inv: lo+1 <= i <= hi+1 && maxval = (Max r: lo <= r <= i-1 : b[r]) //!! maxval is equal to the largest value in b[lo..i-1]if (i == hi+1) break; // Exit test.if (maxval < b[i]){maxval = b[i];} i = i + 1;}// loop post: maxval = (Max r:lo <= r <= hi:b[r])401-22a.4//!! maxval is equal to the largest value in b[lo..hi].401-22a.5while loop form.// precondition lo <= hiint maxval = b[lo];int i = lo + 1;while ( inv() && i<=hi ) // SC eval{// inv: lo+1 <= i <= hi+1 && maxval = (Max r: lo <= r <= i-1 : b[r]) //!! maxval is equal to the largest value in b[lo..i-1]if (maxval < b[i]){maxval = b[i];} i = i + 1;}// loop post: maxval = (Max r:lo <= r <= hi:b[r]) //!! maxval is equal to the largest value in b[lo..hi]. This loop invariant requires a range predicate to show that i = hi + 1 when the loop terminates.for loop form.// precondition lo <= hiint maxval = b[lo];for (int i=lo+1; inv() && i<=hi; i++){// inv: maxval = (Max r: lo <= r <= i-1 : b[r]) //!! maxval is equal to the largest value in b[lo..i-1]if (maxval < b[i]) maxval = b[i];}// loop post: maxval = (Max r:lo <= r <= hi:b[r]) //!! maxval is the largest value in b[lo..hi]. Problem 2.while loop form.// precondition lo <= hiint maxval = b[lo];int i = lo;while ( inv() && i < hi ){// inv: lo <= i <= hi and maxval = (Max r: lo <= r <= i : b[r]) //!! maxval is equal to the largest entry in b[lo..i]i = i + 1;if (maxval < b[i]){maxval = b[i];} }// loop post: maxval = (Max r: lo <= r <= hi : b[r[) //!! maxval is the largest entry in b[lo..hi]The range predicate is not necessary because the exit condition establishes the value of i at termination.401-22a.6401-22a.7Example 3. Note: The product of an empty set of numbers is defined to be 1.while loop form.// Precondition top ≥ 0int i = 0;int prod = 1;while (inv() && i<=top) // SC eval{//inv: 0 <= i <= top+1 and prod = (Prod r : 0 <= r <= i-1 : b[r])//!! prod is equal to the product of the entries of b[0..i-1]prod=prod*b[i];i = i + 1;}// loop post: prod = (Prod r : 0 <= r <= top : b(r))The range predicate is necessary to establish that i = top+1 when the loop terminates.for loop form.// Precondition top >= 0int prod = 1;for (int i =0; inv() && i<=top; i++) // SC eval{// inv: 0 <= i <= top+1 and prod = (Prod r : 0 <= r <= i-1 : b[r])//!! prod is equal to the product of the entries of //!! b[0..i-1]prod = prod * b[i] ;}// loop post: prod = (Prod r : 0 <= r <= top : b[r])Problem 3. Note: The sum of an empty set of numbers is defined to be 0.while loop form.// precondition lo <= hi+1int i = lo;int sum = 0;while (inv() && i != hi + 1) // SC eval{// inv: lo <= i <= hi + 1 and sum = (Sum r: lo <= r < i: b[r])//!! sum is equal to the sum of the entries of b[lo..i-1] sum = sum + b[i] ;i = i + 1;}// loop post: sum = (Sum r: lo <= r <= hi: b[r]) The range predicate is not necessary in this invariant.401-22a.8401-22a.9Problem 4.// precondition lo <= hiint maxindex = lo ;for (int i=lo;inv() ; ){// inv: lo <= i <= hi and b[maxindex] = (Max r: lo <= r <= i: b[r]) // and lo <= maxindex <= i //!! maxindex is the index …