then decrease count by 1. The desired result is the value of sum.

We need to explain how the one new construct works, though by now you

should be able to guess the meaning of “subtractive assignment.”

Chapter 16

Proving programs correct / 463

—¦ Subtractive assignment. An example is the statement, count ’= 1. After

executing such a statement the value of the program variable on the left

is one less than it was before the execution of the statement.

The ¬rst thing we need to prove is that for any natural number n, the proving correctness

of sumDownFrom

program terminates after executing exactly n passes through the loop. This

induction is similar (but easier) than the corresponding proof for sumUpTo,

since it involves a direct induction on the value of count. We leave the proof

as Exercise 16.27.

Now let™s prove that when the program terminates, the value in the vari-

able sum is the sum of the ¬rst n natural numbers, as desired. This will again

require a proof by induction. We will prove that for any k ¤ n, after k itera-

tions of the while loop, the values of the variables sum and count satisfy the

following equation:

(0 + 1 + 2 + . . . + count) + sum = 0 + 1 + 2 + . . . + n

This invariant is a lot more interesting than the one given for sumUpTo. The

new program again accumulates the desired result in the program variable

sum, but the sum is accumulated “downward,” initially n and then adding

n ’ 1, n ’ 2, and so on down to 0, where it stops. The loop invariant re¬‚ects

this by saying that at any time you have to add the missing initial segment

(0 + . . . + count) to the value of sum to get the desired result. But this initial

segment gets shorter and shorter, until ¬nally count = 0 and the program

terminates.

Proof: Basis: After 0 iterations of the while loop, count = n and

sum = 0, and so the equation becomes

(0 + 1 + 2 + . . . + n) + 0 = 0 + 1 + 2 + . . . + n

which is obviously true.

Induction: We assume that the equation holds after k iterations of

the body of the loop, and must show that it holds again after k + 1

iterations of the loop. Let sum be the value of sum after k iterations

of the loop, and sum be the value of sum after k + 1 iterations.

Similarly for count.

Then our inductive hypothesis can be expressed as

(0 + 1 + 2 + . . . + count) + sum = 0 + 1 + 2 + . . . + n

We need to show that this holds for sum and count . After k + 1

iterations, the value of sum is increased by count, and the value of

count is decreased by 1, and so we have

Section 16.5

464 / Mathematical Induction

0 + 1 + . . . + count + sum = 0 + 1 + . . . + (count ’ 1) + (sum + count)

= 0 + 1 + . . . + (count ’ 1) + count + sum

= (0 + 1 + . . . + count) + sum

= 0 + 1+ ...+ n

This concludes our induction.

Finally, we know that when the test condition on the loop becomes false,

count must equal 0, and so at this point 0 + . . . + count + sum = 0 +

sum = 0 + 1 + . . . + n. So after n iterations, the program terminates with

sumDownFrom(n) = 0 + 1 + . . . + n.

These proofs may seem to make heavy going of what are fairly straightfor-

ward facts about the example programs we™ve looked at. True enough. But for

more complicated programs, the kind that actually arise in sophisticated ap-

plications, many such recursive and looping constructions are used, and their

properties can be far from obvious. (This is why software fails so often!) Pro-

grammers must be able to think through such inductive proofs easily, whether

they write them down or not, in order to make sure their programs do indeed

do what they intend.

Exercises

16.27 Prove that when given any natural number n as input, the program sumDownFrom terminates

after exactly n iterations of the while loop.

16.28 Give a proof that the following function computes n!, i.e., the factorial of its argument n. (0!

is de¬ned to be 1, while for any other natural number n, n! = 1 — 2 — . . . — n.)

public natural fact(natural n) {

natural f = 1;

natural count = n;

while(count > 0) {

f—= count;

count ’= 1;

}

return f;

}

The construct f —= count multiplies the value of f by count.

Chapter 16

Proving programs correct / 465

16.29 In the real Java programming language, there is no way to stipulate that a program variable

must contain a natural number. The best that can be done is to specify that the variable must

contain an integer, that is, the value may be positive or negative.

The program below is the same as the sumUpTo example above, except that it uses the

Java keyword “int” to specify the type of the program variables n, count and sum.

Write a speci¬cation for this program, and prove that the program implements the speci-

¬cation. [Hint: it is easiest to decide what the program does when passed a negative number,

and then write the speci¬cation to say that that is what the program should do. Then do the

proof.]

public int sumTo(int n) {

int sum = 0;

int count = 0;

while(count < n) {

count += 1;

sum += count;

}

return sum;

}

16.30 All programming languages have limits on the size of the values that integer typed variables

have. This complicates the job of proving that a real program meets its speci¬cation. The

largest integer available in Java is 232 ’ 1. How would this impact the proof of correctness of

the ¬rst program in this section?

16.31 In this chapter we have not presented a real theory of inductive de¬nitions. Rather, we have

given several examples of inductive de¬nitions, and shown how they are related to proofs

by induction. This is all that most students need. There is, however, an extensive theory of

inductive de¬nitions. In this problem we sketch the start of this theory. The reader interested

in pursuing it further should consult Aczel™s chapter on inductive de¬nitions in The Handbook

of Mathematical Logic.

Let D be some set. By a monotone operator on D we mean a function “ which assigns to

each X ⊆ D a subset “(X) ⊆ D satisfying the following “monotonicity” condition:

∀X ∀Y [X ⊆ Y ’ “(X) ⊆ “(Y )]

We can think of any of our inductive de¬nitions as given by such a monotone op-

erator, and we can think of any such monotone operator as giving us an inductive

de¬nition. The ¬rst four parts of this problem give examples of monotone operators,

the remainder explores the relation between such operators and inductive de¬nitions.

Section 16.5

466 / Mathematical Induction

1. Let D be the set of real numbers and let “(X ) =

X ∪ {x + 1 | x = 0 ∨ x ∈ X}

Show that “ is a monotone operator. Show that “(N) = N, where N is the set of natural

numbers. Show that if “(X) = X then N ⊆ X.

2. Let D be the set of strings made up from the connectives and the propositional letters

used in the de¬nition of the ambig-w¬s. Let “(X) be the set of all propositional letters,

together with anything obtained by one application of the connectives to something

in X. Thus, if A1 A1 ∈ X then the following would all be members of “(X ): ¬A1 A1,

A1 A1 § A1 A1 , and so forth. Show that “ is a monotone operator. Show that if S is the

set of ambig-w¬s, then “(S) = S.

3. Suppose that f is an n-ary function from some set D into D. Let “f (X) =

X ∪ {f (d1 , . . . , dn ) | d1 , . . . , dn ∈ X}

Show that “ is a monotone operator.

4. Let “1 and “2 be monotone operators. De¬ne a new operator by

“(X) = “1 (X) ∪ “2(X)

Show that “ is also monotone.

5. Now let “ be any monotone operator on a set D.

(a) Show that “(“(D)) ⊆ “(D)

(b) Call a subset X of D “-closed if “(X) ⊆ X. By the preceding, we know that there

is at least one “-closed set. (What is it?) Let I be the intersection of all “-closed

sets. Prove that I is “-closed. This set I is thus the smallest “-closed set. It is said

to be the set inductively de¬ned by the monotone operator “.

(c) What is the set inductively de¬ned by the operators in each of 1 and 2?

(d) Let I be the set inductively de¬ned by “. Prove that “(I) = I.

6. Let I0 = …, I1 = “(I0 ), I2 = “(I1 ), . . . , In+1 = “(In ), for any natural number n. These

sets are called the “¬nite iterates” of “. Show (by induction!) that for each n, In ⊆ I,

where I is the set inductively de¬ned by “.

Chapter 16

Proving programs correct / 467

7. In many cases, the set inductively de¬ned by “ is just the union of all these ¬nite iterates.

This is the case with all of the inductive de¬nitions we have given in this book. Why? To

answer this, prove that if “ is “¬nitely based” (in a sense to be de¬ned in a moment), then

the set inductively de¬ned by “ is the union of its ¬nite iterates. Now for the de¬nition.

An operator “ is said to be ¬nitely based provided

∀X ∀x [x ∈ “(X) ’ ∃Y ⊆ X(Y ¬nite § x ∈ “(Y ))]

8. When a monotone operator is not ¬nitely based, one typically has to keep iterating “

“into the trans¬nite” if you want to build up the set from below. Trying to make sense of

these trans¬nite inductions was Cantor™s original motivation for developing his theory of

sets. We have not developed enough set theory to go into this here. But you might like to

try to come up with an example of this phenomenon. You will, of course, need to think

of an operator that is not ¬nitely based.

Section 16.5

Chapter 17

Advanced Topics in

Propositional Logic

This chapter contains some more advanced ideas and results from proposi-

tional logic, logic without quanti¬ers. The most important part of the chapter

is the proof of the Completeness Theorem for the propositional proof system

FT that you learned in Part I. This result was discussed in Section 8.3 and

will be used in the ¬nal chapter when we prove the Completeness Theorem

for the full system F. The ¬nal two sections of this chapter treat topics in

propositional logic of considerable importance in computer science.

Section 17.1

Truth assignments and truth tables

In Part I, we kept our discussion of truth tables pretty informal. For example,

we did not give a precise de¬nition of truth tables. For some purposes this

modeling truth tables

informality su¬ces, but if we are going to prove any theorems about fol,

such as the Completeness Theorem for the system FT , this notion needs to

be modeled in a mathematically precise way. As promised, we use set theory

to do this modeling.

We can abstract away from the particulars of truth tables and capture

what is essential to the notion as follows. Let us de¬ne a truth assignment for

truth assignments

a ¬rst-order language to be any function h from the set of all atomic sentences

of that language into the set {true, false}. That is, for each atomic sentence

A of the language, h gives us a truth value, written h(A), either true or false.

Intuitively, we can think of each such function h as representing one row of

the reference columns of a large truth table.

Given a truth assignment h, we can de¬ne what it means for h to make an

modeling semantics

arbitrary sentence of the language true or false. There are many equivalent

ˆ

ways to do this. One natural way is to extend h to a function h de¬ned on

the set of all sentences and taking values in the set {true, false}. Thus if

we think of h as giving us a row of the reference column, then ˆ ¬lls in the

h

values of the truth tables for all sentences of the language, that is, the values

corresponding to h™s row. The de¬nition of ˆ is what you would expect, given

h

468

Truth assignments and truth tables / 469