Looping with the predicate calculus. How does one determine if a computer program does what it is supposed to do? ... Running test cases can only verify the presence of bugs, never their absence. The predicate calculus is used to develop programs (loops) to solve seemingly difficult problems. The resulting programs are VERIFIABLY CORRECT as well as shorter and clearer than those written using ad hoc heuristics. Knowledge of programming is helpful but not required of the audience.

Here are a few problems to illustrate the type of issues under consideration.

The coffee can problem. A coffee can contains M black beans and N white beans. Repeat the following process as long a possible: Randomly select two beans from the can. If they are the same color, discard them and put a black bean in the can (assume enough extra black beans are available). If they are of different colors, return the white one to the can and discard the black one. Prove the process eventually terminates with one bean in the can. What is its color?

The minimum-sum section problem. Given an array A[0:n-1] of n > 0 integers a minimum-sum section is a nonempty sequence of adjacent elements whose sum is minimal. For example, a minimum-sum section of A[0:4] = [5, -3, 2, -4, 1] is A[1:3] = [-3,2,-4], which has sum -5. The two minimum-sum sections of A[0:4] = [5,3,5,4,2] are A[2:2] and A[4:4]. Given a nonempty array A[0:n-1] write a program - making only one pass through the array - to store in a variable, s, the sum of a minimum-sum section.

The plateau problem. Given a fixed, ordered (by <=) array B[0:n-1] of n > 0 integers a plateau of the array is a sequence of equal values. Write a program - making only one pass through the array - to store in a variable, p, the length of the longest plateau.

The Dutch national flag problem. Given an array D[0:n-1] of n > 0 elements, each of which is "colored" either red, white, or blue. Write a program to permute the elements so that all the red elements are first and all the blue ones last. The color of an element may be tested with Boolean expressions red(D[i]), white(D[i]), blue(D[i]), which return the obvious values. The number of such tests should be kept to a minimum. The only way to permute array elements is to swap two of them; the program should make at most n swaps.

The saddleback search problem.m It is known that a fixed integer x occurs in the fixed, two-dimensional array A[0:m-1,0:n-1]. Further it is known that each row and each column of A is ordered (by <=). Write a program to find the position of x, ie find (i,j) satisfying A[i,j] = x. If x occurs in more than one position, any position will do. Try to minimize the number of comparisons in the worst case.