| 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 |
| Proofs of Correctness of Algorithms |
This is based on material presented during the lectures on Friday, September 12 and Monday, September 15. The objective of this exercise is to help students to understand the ideas that were presented in in these lectures, and to apply them to try to prove the correctness of an algorithm that they may already be familiar with or that is discussed in reference material available to them.
Students needing help with exercise are encouraged to visit the instructor during the instructor’s office hours on September 22. This exercise will be discussed during the tutorial on Monday, September 22.
Consider the following code segment:
// Pre-condition: A is a non-null array of integers // that contains at least one element // Post-condition: max is the largest element in the array A n = A.length; max = A[0] for i from 1 to n-1 do if (A[i] > max) max = A[i]; end do
Write a loop invariant for the loop in this example. Explain how you would prove that this loop invariant is correct.
Explain briefly how you would use this loop invariant to prove partial correctness of this example.
Prove that this loop terminates by giving a loop variant for it. Use the loop variant to give an upper bound on the number of times that the loop will iterate.
Consider a method with name gcd that accepts two integers, a and b as input, and that returns the greatest common divisor of a and b as output.
An interesting pre-condition for an algorithm (to be used to implement this method) would be simply that a and b are integers. A corresponding post-condition would be that the value returned is the greatest common divisor of a and b.
In Question 5 of the tutorial exercise on testing an algorithm for computation of the greatest common divisors is provided. (A definition of gcd that is useful when input integers are zero or negative, that is consistent with this algorithm, is given in the exercise as well.)
This algorithm is (a slight generalization) of the Euclidean algorithm, which is discussed in more detail in pages 192–196 of Susanna S. Epp’s text Discrete Mathematics with Applications — which is commonly used as the textbook for MATH 271 and which is available on reserve at the University of Calgary library. The description of the algorithm that is found there will be helpful as you try to do the following.
Try to prove the partial correctness of this algorithm by using the strategy that has been described in lectures, and by giving intermediate assertions (including a loop invariant) that models what you know about what the algorithm is supposed to do. If you have not yet taken MATH 271 or you are taking it now, and mathematical induction has not been discussed yet, then you might not know how to complete this question. However you should still be able to identify the assertions (corresponding to various lines of pseudocode in the given algorithm) that would be considered in a proof.
One complication, that you will likely notice immediately, is that this algorithm includes an
if … then … else … elsif … else … end if
block of code. Since no proof strategy was given for this type of test, you should begin by rewriting the code so that it uses several
if … then … else … end if
blocks of code to do the same thing, instead.
Describe additional pre-condition-post-condition pairs (corresponding to error conditions that cause error messages to be printed or exceptions to be thrown) that should also be considered when the correctness of the entire program from the previous tutorial exercise is considered. Ideally you should have finitely many pre-condition-post-condition pairs, and exactly one pre-condition should be satisfied when any plausible input is supplied the the user of the program. (Why?)
Prove that the gcd algorithm terminates whenever it is executed when the given pre-condition from the first question is satisfied.
One complication here concerns the possibility that the absolute value of a might be smaller than that of b. Consider a “loop variant” f that is a function of two nonnegative integers, such that
f(n, m) = f(m, n) + 1
whenever m > n ≥ 0.
Then (if you define f in this way) then you only need to complete this definition by specifying the value of f(n, m) when n ≥ m ≥ 0.
As mentioned in class, a loop invariant I(j) can sometimes be used to establish termination, because it is possible to prove that if j is greater than or equal to some value (which bounds the number of executions of the loop body), then I(j) implies that the loop test is false.
Is this true for the loop invariant that you found for the loop in the gcd algorithm, above? Can you modify this loop invariant, so that this is the case?
Now go back and re-examine the program that you wrote (based on the given pseudocode) when working on the previous exercise. Add any assertions that have been suggested by the above process that would improve the documentation of your program and might simplify testing and maintenance of the program later on.
|
This page last modified:
http://www.cpsc.ucalgary.ca/~jacobs/cpsc331/F08/tutorials/tutorial3.html |