401 22 1 COMP 401 Spring 2008 Exercises 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 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 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 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 true int 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 true for 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 hi 401 22 3 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 maxval is equal to the largest value in b lo hi 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 401 22 4 while loop form precondition lo hi int 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 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 401 22 5 while loop form precondition lo hi 1 int 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 hi int 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 true int i 0 while inv b i b 100 inv 401 22 6 i i 1 loop post Problem 7 precondition true int i lo int count 0 while inv i hi if b i value count i i 1 loop post
View Full Document
Unlocking...