Tutorial 11 Lecturer: Ray Reiter Tutor: Andria Hunter =========== 990324 Wed@1pm CSC148, Spring 1999 Tutorial notes, T11 ================================================================== Topics: ------------------------------ - correctness Info for you - Today I finished most of the (new) correctness slides. - Monday I will finish that up, and start big-oh. I'm pretty sure that the other instructors are right with me. This tutorial content will be new to a lot of you, so I've prepared detailed notes. Because it's new, this will probably be the tutorial that you do the most preparation for. (You are getting paid an hour to prepare each tutorial; please let me know whether this has been accurate.) This tutorial might take you a couple hours to prepare for. Please do prepare carefully, because the students may ask you detailed questions. If you have any questions yourself, please email me. I'll be working most of Sunday, so drop by if you want. CORRECTNESS -------------------------------------------------------------------------------- - Very important: study the correctness slides on the web page. Review the following two parts quickly; they've already seen them in class. It's important that you get to the real code, and you can explain more as you go through the examples. So just write up the parts that say "write this". - Remind them that this is a "triple": [write this:] // assertion1 code // assertion2 To show that to show it is a "valid triple", we show that if "assertion1" is true and we execute the given "code", "assertion2" is true. - Put up the anatomy of a loop, along with the four steps necessary to proving iterative code correct. Then explain how steps 1 and 2 rely on induction; step 1 is the base case, and step 2 is the inductive part. Anatomy of a loop: [write this:] // Precondition Q initialization; // Invariant P while( B ) { T } // Postcondition R We usually call B the "loop guard", and T is the "body" of the loop. T is a sequence of zero or more Java statements; they could be assignments, or method calls, or other loops. [write this:] 1) Show {Q init P} is a valid triple 2) Show {P and B T P} is a valid triple 3) Show that P and not B => R 4) Exhibit a bound function t such that: A) t decreases every iteration B) if there are iterations left, t>0 [don't write this, but keep it in mind when they ask questions:] What these four steps really mean: 1) Show that the invariant is true before the loop: that if Q is true and we execute the initialization, then P is true. 2) Show that P is an invariant: that if P and B are true, and we execute the loop body T, then P is true again. 3) Show that the postcondition holds if we are done: that if P is true and B is false, then R is true. 4) Show termination. To do this, we exhibit a bound function t and show that it has the following two properties: A) t decreases every iteration B) if there are iterations left, t>0 A slight change to these four steps gives us rules to develop loops given the assertions: [write this:] 1) Establish the invariant. 2) Find a loop guard B. 3) Make progress. 4) Re-establish the invariant. [don't write this, but keep it in mind when they ask questions:] What these four steps really mean: 1) Given the precondition, find code to make the invariant true: each variable that is mentioned in the invariant but not the precondition will need to be initialized. 2) Find the loop guard: compare the invariant and postcondition, and find out what extra piece of information will tell us we're done. That piece of information is "not B", so to find B we simply negate it. 3) Make progress: define a bound function -- the size of the difference between the invariant and the postcondition -- and find a way to decrease it. 4) Re-establish the invariant: this is the trickiest part; note that it's really the first place we need to actually think about the algorithm. In the loop body, steps 3 and 4 may end up reversed; we may end up doing some work before we decrease the bound function. [write this:] Developing an invariant from a postcondition: 1) Delete a conjunct, or 2) Replace an expression with a fresh variable (In the expression "A and B", "A" and "B" are the conjuncts.) ---------------------------------------------------------------- Here are some problems, along with explanations. For each, note that you don't have to rewrite the code after each step; I just show them this way so that you know exactly what things should look like on the board. A) Given the following pre- and postconditions, come up with an invariant and develop the loop: // Pre Q: 0 <= n, x is a real number. // Post R: p = n*x, and n and x are unchanged. Answer: There's only one conjunct, so it doesn't help to delete it. So we replace n by a fresh variable i: // Pre Q: 0 <= n, x is a real number. // Inv I: p = i*x // Post R: p = n*x 1) Establish the invariant: Compare Q and I, and write down all the new variables: int i = int p = What can we set them to to make p = i*x true? The easiest thing is to set them both to zero; where there is a multiplication, that is often the case: int i = 0; int p = 0; 2) Find a loop guard B. What piece of information do we need to know to show that we're done? Comparing I and R, we immediately see that if i == n then we're done. So we're not done when !(i==n): // Pre Q: 0 <= n, x is a real number. int i = 0; int p = 0; // Inv I: p = i*x while ( !(i==n) ) { 3) Make progress. We note now that i started off at 0, and it finishes at n. So it needs to increase in the loop. Our first guess at a bound function t is, therefore, n-i. We need to make t decrease; we can add 1 to i, which again for a multiplication is often the way to go: // Pre Q: 0 <= n, x is a real number. int i = 0; int p = 0; // Inv I: p = i*x while ( !(i==n) ) { i = i + 1; This brings us to step 4: 4) Re-establish the invariant. Note that after we increment i, p == (i-1)*x. So we need to change p to make it catch up, and we do this by adding x to p: // Pre Q: 0 <= n, x is a real number. int i = 0; int p = 0; // Inv I: p = i*x while ( !(i==n) ) { i = i + 1; p = p + x; } // Post R: p = n*x B) Last fall's exam question. This sorts an array containing only the numbers 1, 2, and 3, but it does it in linear time. Draw a picture of the array!!! Postcondition: 0 a b c n-1 ------------------------------------- list | 1's | 2's | 3's | ------------------------------------- Even if they can't come up with the invariant, they should be able to tell you how we did it. (Replace b+1 with a fresh variable c.) They may want to replace both a+1 and b+1 with two fresh variables, but that would mean that b was completely unanchored and we wouldn't know what to initialize it to. They may also want to replace a+1 instead of b+1; that works out almost the same, except we'd be working from the right side. // Precondition: n >= 0 && list[0 .. n-1] contains 1's, 2's, and 3's in // any order. int a = -1; int b = -1; int c = n; // Invariant: // list[0 .. a] == 1 && // list[a+1 .. b] == 2 && // list[c .. n-1] == 3 // bound function: c - b; we can decrease it with either b=b+1 or c=c-1. while ( b+1 != c ) { if ( list[b+1] == 1 ) { a = a + 1; b = b + 1; // swap list[a] and list[b] int temp = list[a]; list[a] = list[b]; list[b] = temp; } else if ( list[b+1] == 2 ) { b = b + 1; } else if ( list[b+1] == 3 ) { c = c - 1; // swap list[b+1] and list[c] int temp = list[b+1]; list[b+1] = list[c]; list[c] = temp; } } // Postcondition: // list[0 .. a] == 1 && // list[a+1 .. b] == 2 && // list[b+1 .. n-1] == 3 Invariant picture to draw: 0 a b c n-1 ------------------------------------- list | 1's | 2's | unknown | 3's | ------------------------------------- Precondition picture to draw: a b 0 n-1 c ------------------------------------- list | unknown | ------------------------------------- Postcondition picture to draw: 0 a b n-1 ------------------------------------- list | 1's | 2's | 3's | ------------------------------------- C) Harder problem, but they should get the invariant, the initialization, and the loop guard with only a little help. // Pre Q: b >= 0 and c >= 0 // Post R: b = q*c + r and 0 <= r < c Find the invariant by deleting a conjunct. There are three to consider: b = q*c + r and 0 <= r, and r < c. Deleting the first one gets rid of most of the real information; it relaxes the postcondition *too* much. Of the latter two, we choose to delete r < c: // Inv I: b = q*c + r and 0 <= r 1) Establish the invariant: What can you set q and r to to make P true? Again, we have a multiplication, so we try q = 0. The equation then states b = 0*c + r, so we can set r to b: // Pre Q: b >= 0 and c >= 0 q = 0; r = b; // Inv I: b = q*c + r and 0 <= r 2) Find a loop guard B. What piece of information do we need to know to show that we're done? The only difference is exactly the conjunct we deleted: r < c. So we negate it: // Pre Q: b >= 0 and c >= 0 q = 0; r = b; // Inv I: b = q*c + r and 0 <= r while ( !(r < c) ) { 3) Make progress. We note that we're done when c > r, so we try r - c as our bound function. We need to decrease it, and that can be done one of two ways: r = r-1; and r = r-c; Noting that the other part of the equation also deals with increments of c, we choose the latter: // Pre Q: b >= 0 and c >= 0 q = 0; r = b; // Inv I: b = q*c + r and 0 <= r while ( !(r < c) ) { r = r - c; 4) Re-establish the invariant. We've broken the equation; now b = q*c + r + c. In order to fix it, we increment q: // Pre Q: b >= 0 and c >= 0 q = 0; r = b; // Inv I: b = q*c + r and 0 <= r while ( !(r < c) ) { r = r - c; q = q + 1; } // Post R: b = q*c + r and 0 <= r < c [ALH NOTE: Why b = q*c + r + c above? The reason is that we've decremented c, so b is now relatively larger. To bring it back into line, we suck that "+c" into the "q*c" part by adding one to q.]