| home page - news - syllabus - schedule - assignments - tutorials - tests - java - references - Mike Jacobson |
| Tutorial 1 - Tutorial 2 - Tutorial 3 - Tutorial 4 - Tutorial 5 - Tutorial 6 - Tutorial 7 - Tutorial 8 - Tutorial 9 - Tutorial 10 - Tutorial 11 - Tutorial 12 - Tutorial 13 - Tutorial 14 - Tutorial 15 - Tutorial 16 - Tutorial 17 - Tutorial 18 - Tutorial 19 - Tutorial 20 - Tutorial 21 - Tutorial 22 - Tutorial 23 |
| Proofs of Correctness of Algorithms |
This exercise can be used to students to make sure that they understand the basic concepts concerning proofs of correctness of algorithms that have been discussed in class.
Students should read through this exercise, and spend time trying to solve the problems on it, before attending the tutorial.
The following problems test comprehension and ability to apply material presented during the lectures on correctness of algorithms.
It is to be expected that all of the problems in this first section can be solved by any student who has successfully completed the prerequisites for this course, attended the lectures in which correctness of algorithms have been discussed, and carefully read through the material about this that is now available.
Teaching assistants will not be spending very much time in tutorials discussing these problems! Students should look at them anyway to make sure that they understand these problems and know how they should be solved.
Students who do have difficulty with these questions should contact the course instructor or attend the instructor’s office hours in order to discuss these! Students lacking the desired background in mathematics can certainly be helped, but only if the instructor knows that they need this.
State the definition of each of the following.
Explain how “correctness,” “partial correctness,” and “termination” are related.
Give truth tables for each of the following expressions. (Consult your textbook for MATH 271 or 273, or one of the references for discrete mathematics recommended for this course if you do not know what a “truth table” is.)
The expression “p ∨ q” is spoken aloud as “p or q,” and the expression “p ⇒ q” is spoken aloud as “p implies q.” Do these expressions have the truth values that you would expect, considering this information?
If they do not always have the truth values you would expect then how (and when) are they different than expected?
Are the following expressions well defined? What else (beyond the material presented in the lecture notes) would you need to interpret these?
This problem might be helpful if you were not sure about your answer for the previous one: Show that the following two expressions have different values when p is false.
Some (but not all) of the logical operators we are considering are available as operators in Java.
How is the expression
p ∨ q ∧ r
expressed in Java (as a function of p, q, and r)?
If you did not add parentheses, but simply replaced the operators ∧ and ∨ with their equivalents in Java, then the result is equivalent either to
(p ∨ q) ∧ r
or
p ∨ (q ∧ r)
Which one? Why?
You should have seen propositional logic in a prerequisite course such as MATH 271 or 273 (or PHIL 279 or 377). However, some of the notation is probably different! For your own reference, summarize the differences in notation that you find when comparing the presentation of propositional logic in these courses.
Recall that the proof rules introduced in class can be used to reduce the problem of proving the correctness of algorithms to that of proving claims that do not have anything to do with algorithms at all (and that can be proved using the kind of proof techniques introduced in MATH 271 or 273).
List the claims that should be established to conclude each of the following.
Which of the programs listed in the previous question are partially correct?
The following longer problem will be discussed during the tutorial. It is an attempt to give a slightly more realistic picture of how the material that has been introduced in lectures might be used: Rather than starting with undocumented code (or code along with the precondition(s) and poscondition(s) for the problem to be solved by it) this begins with an informal description of an algorithm, and a sketch of a proof that it does what it should, and asks you to produce a program along with a proof of its correctness from that.
Consider the “Search” problem that was introduced as an example at the beginning of the lecture notes on this topic.
This problem was specified by a pair or preconditions and postconditions that are listed again below.
Precondition P1: Inputs include
- n: a postive integer
- A: an integer array of length n, with entries A[0], A[1], …, A[n−1]
- key: An integer found in the array (ie, such that A[i] = key for at least one integer i between 0 and n−1)
Postcondition Q1:
- Output is the integer i such that 0 ≤ i < n, A[j] ≠ key for every integer j such that 0 ≤ j < i, and such that A[i] = key
- Inputs (and other variables) have not changed
This pair of precondition and postcondition describe what should happen for a “successful search.”
Precondition P2: Inputs include
- n: a postive integer
- A: an integer array of length n, with entries A[0], A[1], …, A[n−1]
- key: An integer not found in the array (ie, such that A[i] ≠ key for every integer i between 0 and n−1)
Postcondition Q2:
- A notFoundException is thrown
- Inputs (and other variables) have not changed
This pair of precondition and postcondition describe what should happen for an “unsuccessful search.”
One, very widely used, algorithm for this problem is a “linear search:” compare the given key to A[i] for increasing i — that is, for
i = 0, 1, 2,…
— until you either discover an integer i such that 0 ≤ i < n and A[i] = key (so that i is the value that should be returned — because you checked values in increasing order and this is the first such value that you discovered), or until you have checked all the array entries (so you know that key is not stored in the array, and an exception should be thrown).
Write code (using pseudocode as used in the lecture notes, but that also includes statements to return values and to throw exceptions) for the linear search algorithm that has been described above.
Your code will very likely consist of one or two lines at the beginning to initialize one (or two) variables, followed by a while loop in which most of the work is done. The body of this loop will probably include a return statement that is called if the search is successful. The value of some variable will probably be incremented every time the end of the loop body is reached.
The code will probably end with a statement after the loop — where an exception is thrown to indicate that the search was unsuccessful.
Using the informal description of the algorithm that has been given, try to identify all the intermediate assertions that hold after each statement in your program is executed.
One of the trickiest, but most important, of these assertions will be the “loop invariant.” If it is not clear what this should be right away then you should make up an input (corresponding to an unsuccessful search, or a successful search where the key is not found right away) and then trace the beginning of the execution of your program by hand. Write down all the information that you know at the beginning of the first, second, and third executions of the loop body. See whether there is a pattern that you can identify that will help you to write down what is know after the kth execution of the loop body, for larger k.
Another very important assertion will be the one that holds immediately before the return statement in the loop body — this should imply that the output (that is about to be returned) is correct.
Once you believe that you have discovered the assertions that are needed, try to complete a proof of “partial correctness.” You may need to cycle back and forth, once or twice, between this step and the previous one, because your assertions are not strong (or complete) enough for a proof to be written down.
You can do this by considering each precondition-postcondition pair separately — considering successful searches, and unsuccessful searches, as separate cases. Howeever, you will probably discover that most of what you need to prove (about your algorithm) is the same for each case.
Finally, try to identify a “loop variant” for the loop in your program and use this to prove termination as well.
|
Last updated:
http://www.cpsc.ucalgary.ca/~jacobs/Courses/cpsc331/W12/tutorials/tutorial2.html |