COMP 401,Spring 2008401-22.1COMP 401,Spring 2008Exercises for Chapter 3 You should complete this exercise by the end of February. I suggest you try the exercises before you look at the answers. Nothing to turn in. Feel free to collaborate.Loop 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, 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;}401-22.2// loop post: (Ar: 0 <= r <= 100: b[r] == 0) //!! All entries in b[0..100] are equal to 0.(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.Problem 1.while(true) loop form.// precondition trueint i = 0;while (true){b[i] = i;// inv:if (i == 100) break;i = i+1;}// loop post: //!! 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:if (i == 100) break;}// loop post: //!! Each entry in b[0..100] is equal to its index.Example 2. while(true) loop form.// precondition lo <= hi401-22.3int 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]) //!! maxval is equal to the largest value in b[lo..hi].while 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.401-22.4while loop form.// precondition lo <= hiint maxval = b[lo];int i = lo;while ( inv() && i < hi ){// inv: i = i + 1;if (maxval < b[i]){ maxval = b[i];} }// loop post: Example 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.401-22.5while loop form.// precondition lo <= hi+1int i = lo;int sum = 0;while (inv() && i != hi + 1) // SC eval{// inv: sum = sum + b[i] ;i = i + 1;}// loop post: Problem 4.// precondition lo <= hiint maxindex = lo ;for (int i=lo;inv() ; ){// inv: if (i==hi) break;i = i + 1;if b[maxindex] < b[i]maxindex = i;}// loop post: Problem 5.// precondition true// old_b = b // The array old_b records the original value of b. int i = 1 ;while (true){b[i] = b[i-1] + b[i] ;i = i + 1 ;// inv: if (i == 101) break;}// loop post: Problem 6.// precondition trueint i = 0 ;while ( inv() && b[i] != b[100] ){ // inv:401-22.6 i = i+1;}// loop post:Problem 7.// precondition trueint i = lo ;int count = 0 ;while ( inv() && i <= hi ){ // if (b[i] == value) {count++;}i = i+1;}// loop