401 22a 1 COMP 401 Spring 2008 Answers to exercises for Chapter 3 Loop invariant exercises Each 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 true int 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 true for 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 3 Problem 1 while true loop form precondition true int 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 true for 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 hi int 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 5 while loop form precondition lo hi int 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 hi int 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 hi int 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 6 401 22a 7 Example 3 Note The product of an empty set of numbers is defined to be 1 while loop form Precondition top 0 int 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 0 int 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 1 int 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 8 401 22a 9 Problem 4 precondition lo hi int maxindex lo for int i lo inv inv lo i hi and b maxindex Max r lo …
View Full Document
Unlocking...