David Gries
gries@cs.uga.edu
After almost 20 years, this is still one of the best and simplest examples of the use of formal programming methodology, used in an informal but precise way. In the past, I sent the problem to many people. Those that thought in terms of the formal development of programs returned the solution almost immediately; few of those that didn't were able to find a suitable solution.
Given is an integer x and a two dimensional array b[0..m-1, 0..n-1] of integers. Each row and each column is in non-descending order. For example, here is one possible array, with m=4 and n=4:
Value x is known to be in b. Desired is an algorithm that finds a location of x in array b. Thus, given precondition
b
0 1 2 3 n
0 1 2 3 m
2 2 3 5 3 4 5 6 3 5 6 8 3 6 7 9
Q: x is in b[0..m-1, 0..n-1]the algorithm is to store values in variables h and k to truthify
R: x = b[h, k] .
Development of the algorithm.
Try solving the problem yourself before proceedng!
A loop or a recursive procedure is needed to search b for x. We decide on using a loop, and we need a loop invariant. The loop invariant is a generalization of R and Q, and to find a suitable generalization, we notice that R can be rewritten so that it has the same shape as Q:
R: x is in b[h..h, k..k] .Q says that x lies in a big rectangle; R says that x lies in a small rectangle. Perhaps the loop invariant P states that x lies in a rectangle. We write such an invariant by making a copy of R in which two of its expressions are replaced by fresh variables.
invariant P: x is in b[h..i, j..k]This leads to an amzingly simple algorithm, whose execution time in the worst case is proportional to m+n. We leave the development to you --don't forget to use the fact that the rows and columns are in non-descending order. What results is the following, given in guarded command notation and also as a more conventional while loop.
| h, k:= 0, n-1;
{invariant P: x is in b[h..m-1, 0..k]} do b[h,k] < x --> h:= h+1 [] b[h,k] > x --> k:= k-1 od |
h, k:= 0, n-1;
{invariant: x is in b[h..m-1, 0..k]} while x != b[h, k] do if b[h, k] < x then h:= h+1 else k:= k-1 |
Remarks
The development of this algorithm is made possible by the use of a formal programming methodology proposed by Edsger W. Dijkstra in 1975 --see his monograph "A Discipline of Programming". Gries's text "The Science of Programming" (1981) makes the material accessible to undergrads. The material is not difficult, and several colleges and universities teach the material to freshmen. However, the methodology does call for changing one's thought habits, rather than just learning facts, and many people are unwilling to change --we all know Mark Twain's comment, "Nothing needs changing so much as the habits of others.".
The methodology requires the ability to calculate with formulas. Here, we did not need to do much. We just noticed that R could be rewritten so that it had the same shape as Q, and then we generalized the new version of R into the loop invariant. Such calculation is easily within the reach of even freshman CS students. However,
Calculation has to be taught.And this calls for teaching logic as a tool, instead of as just another area of study. As Gries and Schneider say in their text "A Logical Approach to Discrete Math",
Logic is the glue that binds together arguments in all domains.Almost all arguments use implication, conjunction, disjunction, negation, and often quantification, and one needs to know how to calculate in the domain of booleans. Teaching calculation using "A Logical Approach to Discrete Math" in a freshman-sophomore discrete math course is the best way to ensure that your students understand logic and calculation in the practical sense of the word. For more information, see the web page http://www.cs.uga.edu/~gries .