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.]