Program Correctness Proofs in a
Computer Literacy Course

David Arnow
Department of Computer and Information Science
Brooklyn College City University of New York
Brooklyn, New York 11210
e-mail: arnow@sci.brooklyn.cuny.edu
Abstract. Program correctness proofs have recently been successfully added to Brooklyn College's required course on mathematical and computer literacy for the general student. This topic significantly integrates the mathematics topic of the course (logic) with one of the computer science topics (programming).
The students are prepared mathematically for studying correctness proofs through a treatment of elementary sentential logic that is presented both in the context of and in contrast to everyday reasoning. Included in this treatment are elementary logic proofs and problem-solving strategies appropriate for constructing proofs.

Before doing program correctness proofs, students also study a very small subset of a programming language, essentially consisting of assignment, iteration and simple input/output. Iteration is always restricted to the while loop, which is explained both operationally and, in an informal way, axiomatically. Loop invariants are introduced from the outset. So far two different languages have been used in this effort: Pascal and the Bourne Shell language. Both seem to be equally effective.

The inclusion of program correctness proofs in the curriculum has been deemed a success because testing and homework assignments show that all students are able to understand what a program correctness proof is; most students are able to fill in blank pieces of proofs that are partially done; about a quarter of the students are able to write their own. The students are for the most part urban working-class students, roughly 45% minority. Many are immigrants from third world or eastern European countries.

This success has important lessons not just for computer literacy instruction but for computer science instruction as a whole: students with weak academic backgrounds can approach and appreciate this material, if it is presented in the right way and if they are given the necessary prerequisite ideas.

Publication Information: This Brooklyn College Technical Report was presented at the November 1992 IEEE Frontiers in Education conference and appeared in the conference proceedings: Program Correctness Proofs in a Computer Literacy Course. Proceedings of the IEEE Frontiers in Education '92 Conference. Nashville, Tennesse, November, 1992.

Acknowledgment of Support: This work was made possible by an undergraduate curriculum development grant from the National Science Foundation , CISE Division (USE-9150719).

INTRODUCTION.

The goal of this project has been to incorporate a treatment of program correctness proofs into a required general education course on mathematics and computer science for non-science, non-math/computer science majors.

There were two reasons for undertaking this. First, although an earlier version of this course successfully presented a number of important ideas from computer science, it leaned far too much in presenting a strictly operational view of programming. It was therefore desirable to balance this with a formal or axiomatic view. Second, the mathematics part of the course is sentential logic. It was useful apply the latter in an arena that the students had not yet encountered (as distinct from logic proofs or geometry) but in one that the students could quickly become familiar with in an informal way.

The population. The Brooklyn College students reflect an urban, ethnically heterogeneous working-class population. The College ranks fourth in the nation (including degrees issued from historically black colleges) in awarding baccalaureate degrees to African-Americans. 21% of the undergraduates are African-American, 11% are Hispanic and 11% are Asian. Many students are immigrants and English is not the native tongue for many. 55% of our freshmen are required to take remedial courses to correct skills deficits in mathematics, reading or writing.

Most of our students have specific weaknesses that make the task appear daunting. The students have very little experience with abstraction. The course implementation has to take this into account in every topic. Every abstraction, whether it is a rule of inference or an algorithm for multiplying must first be introduced and afterwards reinforced with numerous concrete examples. In teaching very elementary programming this is a situation that is fraught with danger. That's because the most casual kind of concrete approach to explaining programming language constructs and programs leads very readily to a strictly operational view of the subject. The challenge then is to be pedagogically concrete without having one's curricular goals subverted.

Prior to this course most students have no experience with writing, reading or understanding proofs or programs. Most do not know what a proof is and have only a vague idea of what a program is.

The student population does, however, have special strengths of its own that make the task easier to approach than it might be in other contexts.

First, there are no "hackers" (in the good sense of the word), that is there are no students who see themselves as nearly expert programmers. Such students typically have no patience with a disciplined approach to programming, but rather are on the lookout in their classes for extra tricks or hand-holding through new technology. Although some of our students are often eager to write and run programs, none are in so much of a hurry that they are unwilling to make what others might consider detours. Nor does this population feel it has nothing to gain by learning about a systematic approach- these students know they need all the help they can get in writing programs.

The absence of experience with programming in general means that the students are not wedded intellectually to the operational perspective in understanding programs and programming language constructs. Only those who have attempted to teach an axiomatic approach to students with years of operational-only instruction can appreciate what an advantage this is. These students are open to both approaches.

The majority of this population by definition will not take additional math or computer science courses. This frees the course designer from the constraint of coverage- there aren't a dozen topics that must be covered in preparation for the next course. Thus, if a topic, such as program correctness proofs, is deemed important, as much time as necessary may be taken to teach it properly.

Furthermore, the rest of the course can be geared, at least in part, as preparation for this topic.

PROGRAM CORRECTNESS PROOFS IN CS EDUCATION.

Since there is no consensus on the proper role of program correctness proofs in computer science and software engineering, it not too surprising that the place for this topic within the CS curriculum is disputed. Still, even if it turned out that these proofs themselves have no value in day-to-day practice, it is quite possible that the perspective that their study offers would be of practical value. However, even if that were not the case, it is still possible that their study by someone outside the field could clarify the outsider's view of CS. That is the view that I take in this work. Furthermore, the experience from this course has some bearing on the debate concerning the place of correctness proofs in the CS curriculum. For, the success of this work shows that teaching this material is possible, and so the debate must center strictly on the value of the material, not its pedagogical feasibility.

CORRECTNESS PROOFS IN A GENERAL EDUCATION COURSE.

The course in question is an attempt appropriate place for mathematics and computer science within Brooklyn College's widely recognized Core Curriculum [for example, see Cheney, 1989], a set of specifically designed general education courses that are required of all students at the college. In fact, the design of this course was in part inspired by that of the required courses in classics, history, music, political science and other liberal arts [Arnow, 1991]. Our main purpose is to offer the general student ideas from our discipline that are interesting and of enduring value. This is the best way to Organization and topics of the course. The first half of the course is a study of elementary propositional logic which emphasizes the connections and differences between logic and "everyday" reasoning, the significance of language and language issues such as ambiguity, the utility of symbolic and formal methods, and the distinction between form and content. Though that constitutes the mathematics component of the course, these themes are repeated in the second half of the course, the computer science component.

The first part of the computer science component of the course includes a discussion of machine representation of information, numeral systems, logic gates and circuits. Here the students apply the logic introduced earlier and learn to use Disjunctive Normal Form as a means of methodically designing circuits.

Following this, the students are taught a tiny subset of the Pascal language: integer variables, the readln, writeln, while statements, and comments. This subset is taught in a relatively formal fashion. The tokens and token classes are first introduced. After this, the syntax is introduced, and then the semantics of the subset are explained. The concept of an invariant is taught immediately, though informally, and the meaning of the while statement is explained with an eye to the correctness proofs later in the course.

A number of programs which build on the theme of achieving complexity by repetition of simple operations are developed. These invariably include addition by repeated counting, multiplication by repeated addition, etc. Since the student already has seen how hardware can add, he or she has a vision of how operations as complicated as logarithms and exponents can be carried out and how they ultimately are based on a few very elementary primitives. These programs also serve as good examples for building programs by identifying loop invariants.

In this context it is easy to see how important a discussion of correctness proofs can be. For, on the one hand the first part of the computer component shows the students how formal methods (truth tables, DNF, etc.) can be used to design hardware. Failure to similarly put formal methods to good use in the programming part would lead to the mistaken idea that programming is a hit-or-miss affair or at least that program correctness is strictly an empirical matter.

Correctness proofs also provide a good opportunity to demonstrate the importance of mathematics. Students tend to accept computers as important because they are highly visible. As was achieved in the discussion of circuits, correctness proofs offer a concrete example of the utility of mathematics to other fields.

Finally, for this particular course, a discussion of program correctness proofs offers a nice way of tying the various themes and ideas of the course together. The students' understanding of proofs is reinforced in a new, but accessible, context. The theme of building complex structures from simpler ones (proofs from lemmas) and formalizing that which we understand formally reoccur.

ACHIEVING SUCCESS.

To successfully teach this material it is necessary to ensure that the students have the necessary intellectual background, to motivate the students and alert them to the material's significance and to develop the material in a step-by-step fashion so that the instructor is always communicating at the level of the student.

Prerequisites. In the end we identified three areas that the students needed to be familiar with in order to approach program correctness proofs. First, they had to be familiar with logical connectives, negation, rules of inference, and proofs. These concepts were already covered in the beginning of the course, before correctness proofs were introduced into the curriculum. Second, it turned out to be useful to explicitly discuss problem-solving strategies in the context of writing proofs. In particular, the students needed to learn to "work backwards", that is, given a desired conclusion and a set of axioms and rules of inference, they had to be able to construct the steps of a proof going from conclusion "backwards" to axioms. This is essential is working with the assignment statement for example. Before the inclusion of correctness proofs, the logic proofs handled in the logic part of the course sufficiently simple that little explicit attention was paid to strategy. Now we prepare students for working backwards from the beginning of the logic part of the course by giving them "missing premise" problems such as:
(1) If the polls are right then the challenger will win.
(2) missing premise
Conclusion: The polls were wrong.
Directions: Identify the (missing) premise that will make this a valid argument.

So, by modifying the logic part of the course to rectify that omission, the students were better prepared for correctness proofs.

Finally, students needed to be accustomed to making informal arguments about the correctness of programs prior to being introduced to a more formal approach. The idea of a loop invariant and the semantics of a while statement had to be "second nature" to them. In order to guarantee this, the part of the course that teaches elementary programming had to be modified [Arnow, 1991].

Motivation. All students, even "motivated" students, need challenging material to have a motivation. Motivating correctness proofs is relatively easy. It is not hard to come up with famous example of software catastrophes that students have either heard of or can readily appreciate. Along with a brief discussion of society's increasing dependence on computer software, this clearly underscores the importance of correct programs. The inadequacy of (at least casual) testing for these student can be related to fallacies they have learned earlier in the course:
If the program is correct then the test will succeed.
The test succeeds.
The program is correct. (Fallacy of Affirming the Consequent.)
And it is not hard to come up with examples that illustrate this.

Development of the material. Most important is the way the material itself is taught. The material must be presented in small, easily digested pieces. Students must have the opportunity to become familiar with essential concepts and terminology before additional demands are made. A useful aid for the instructor and the student, to ensure that these microsteps are indeed microsteps and to verify that they have been mastered is the use of checkpoint exercises. The remainder of this section describes the small steps that we take and gives examples of checkpoint exercises for those steps.

Acquaintance with correctness proofs. Before developing the topic in any significant way, the students are introduced to the format we use and to the idea of assertions about the values of variables at specific points in the program text.

checkpoint exercise: 
		Given the following program fragment:	  #2	x:=5;
		(for reference, statements are 		  #3	y:=x+1;
		numbered with sharp signs)			     #4	x:=x+y
and the proof fragment below, identify those assertions in the proof that you would agree with
(ignoring the reason given for each step): 
				step	   assertion			reason
				(4)	 x<8 right after #2		[#2,1: rule]
				(5)	 x>8 right after #3 		[#3,1: rule]
				(6)	 x>8 right after #4		[#4,1: rule]
				(7)	 y=6 right before #3		[#3,1: rule]
				(8)	 y<9 right after #3		[#3,1: rule]


Assignment statement structure. The student is reminded of the distinction between the left and right hand sides of the assignment statement and is introduced to the terminology "target" and "expression".

checkpoint exercise:
For each of the assignment statements below, identify the target and the expression: 
			...
			sum := a+b
			...

The Assignment Rule. The student is introduced to the Assignment Rule:
(1) assertion P involving expression e is true before statement #N
(2) statement #N is x:=e
(conclusion) after statement #N any assertion Q is true provided that
Q can be transformed to P by replacing every mention of x with e.

terminology: the assertion with e in (1) is called the precondition
the assertion with x in the conclusion is called the post condition.
checkpoint exercise:
For each argument below, indicate whether or not it is a valid application of the
Assignment Rule and explain.
...
(1) total=prod right before #3
(2) #3 is x:=y
(conclusion) total=prod right after #3
(1) x=z+w right before #8
(2) #8 is y:=x  
(conclusion) y=z+w right after #8
(1) big<6 right before #9
(2) #9 is bigger:=big+1  
(conclusion) bigger<7 right after #9
(1) y=z+4 right before #8
(2) #8 is y:=x  
(conclusion) x=z+4 right after #8

Missing premise problems. The student has been familiar with this type of problem from the beginning of the course. Now it is applied to the assignment rule in preparation for developing proofs later on.
checkpoint exercise:
Missing Premise Problems. In the example below, there is a missing premise
(the precondition). Replace the question marks ??? with the missing premise to
make the argument a valid application of the Assignment Rule.
(1) ???
(2) #8 is side1:=side2  
(conclusion) side1>side3 right after #8

Checking proofs by examples. In this step, a rule is given for making assertions about statements that are consecutive and the student is introduced (again) to small proof fragments (concerning fragments of programs that contain just assignment statements). This time however, the student is taught to verify that the proof argument is a valid application of the assignment and consecutive statements rules.

checkpoint exercise:
Given the following program fragment: #1 a := 1;
#2 b := 1;
#3 c := a+b;

check each step that involves the Assignment Rule by writing the step in
unabbreviated form and verifying that it is a proper application of the rule:

Step Assertion Justification
(1) 1+1=2 before #1 [Kindergarten]
(2) a+1=2 right after #1 [#1,1: Assignment Rule]
(3) a+b=2 right after #2 [#2,2: Assignment Rule]
(conclusion) c=2 right after #3 [#3,3: Assignment Rule]

Writing small proof fragments. Having become familiar enough with the assignment rule and the consecutive statements rule, and having become experienced in checking proofs, the student starts to write her own.

checkpoint exercises:
Given the following program fragment: #1 count := 12;
#2 num := 0
prove that count+num=12 after #2

Given the following program fragment: #4 count := count-1;
#5 num := num+1
what precondition for #4 is required in order for count+num=12 right after #5


Loop Invariants. The student has already been introduced to loop invariants in the programming part of the course. In fact, students are encouraged to use loop invariants to help guide them in writing their code. Students are required to identify relevant loop invariants in any program they submit. In this step, the students are given the "invariant rule" which formally defines what is required for an assertion to be a loop invariant. In practice, for the examples here, it means essentially writing two mini-proof fragments: one to show that the assertion is true before the while statement, the other to show that if it is true before the loop body, then it will also be true after the loop body. We don't however yet demand that they identify the loop invariant themselves (although many probably could already do so.)

checkpoint exercise:
Given program fragment
prod:=0;
count:=0;
while count<a do begin
prod:=prod+b;
count:=count+1
end
show that prod=count*b is a loop invariant.


Loops. The "while rule" is given in this step: after the while statement all loop invariants are true and the loop condition is false. This is just a formalization of what the students have learned when the while statement was introduced to them during the programming part of the course.

checkpoint exercise:
In an earlier exercise you proved that quot*a+rem=b is a loop invariant in:
quot:=0;
rem:=b;
while rem>a do begin
quot:=quot+1;
rem:=rem-a
end
Use that result as a lemma to prove that at the end of this fragment if rem is equal to 0, quot=b/a.

DEFINING SUCCESS.


In teaching program correctness proofs, the naive, material-oriented definition of success might be the ability of the student to be given a program and write a correctness proof for it or to develop a correctness proof concurrently with a program. However, in a project like this, it is important that success be defined in a student-oriented way, that is in a way that takes into account the students' needs and the purpose for providing them this material.

The students in this course for the most part will not be programmers and computer scientists. They will certainly not need to write correctness proofs, whether in conjunction with program development or not. The purpose for including this material in the course is to present the formal view of programs, to demonstrate the application of mathematics in computer science, and to provide examples of proofs outside the areas that they have already experienced (logic proofs in this course, possibly geometry proofs from earlier study). To verify that these goals have been reached, it is not necessary to test whether or not a student can develop a proof concurrently with a program.

PROBLEMS


The course in question is offered by the Math and Computer Science departments. The latter, even with the nation-wide drop in computer science majors is still understaffed with respect to its undergraduate and graduate programs. Although the original mandate for the Brooklyn College Core Curriculum demanded that only full-time faculty from an appropriate department teach the course, fiscal and personnel realities force the department to staff the course with adjunct instructors, graduate students and faculty from other departments as well.

CONCLUSION


Mathematics and Computer Science. In Brooklyn College, the marriage between mathematics and computer science in the general education course has been an uneasy one. Some faculty (primarily from the math department) have viewed the course as one where the computer is a tool for illustrating mathematical concepts. Others (also from the math department) sought to use the computer as an alternative approach to problem solving (simulation vs. analysis). Neither view is appealing to computer science faculty who want to provide a non-cookbook view of their field.

The success we have had in treating this topic indicates that another avenue is available. That is, computer science can be treated mathematically, even at this level. Again, illustration of mathematical ideas (proof, axioms, etc.) is involved. However, the benefit to the teaching of mathematics but goes beyond illustration: the students themselves are active and write proofs (or parts thereof). They get an opportunity to apply these ideas to an area that is both new to them but also concrete.

The benefit of this approach from a computer science point of view is clear. Having studied programs from both an operational and a formal approach, the students leave the course with a vision of computer science as both an engineering and a mathematical discipline.

Feasibility of the topic. The experience at Brooklyn College shows that teaching program correctness in a general education course is feasible even for relatively weak students, provided that: These results also are important for the debate concerning the formal approach among teachers of undergraduate computer science. For surely if the students in the general education course can master this material, there is no question that, if properly approached, computer science majors can as well. Feasibility is not an issue; the debate must focus strictly on the merits of the formal approach itself. For myself, just as I would find it regrettable for the general education student to miss a chance to see both the formal and operation approach, I find it unpardonable for computer science majors to lose that opportunity.

Undertaking to teach program correctness proofs in this course would have been impossible were it not for a conscious decision to take a principles-based approach to the subject advocated by REFERENCE, and modified as described in [Arnow, 1991]. This view of computer literacy, therefore, continues to be rewarding both to instructor and student. The rewards, however, do not have to stop here. Computer science and its intersection with mathematics is an intellectually rich area that has only begun to be mined for the general public. We are limited only by the finite number of credits in our courses and by our relative inexperience in arranging and presenting the subject matter.

Acknowledgments. Carroll Zahn of the Computer Science Department (Pace University) first suggested to the author that a discussion of program correctness might be appropriate for the general education course. Paula Whitlock of the Department of Computer and Information Science (Brooklyn College) was foremost among the Brooklyn College faculty in introducing this material in her classes and in giving useful feedback on student response to the material.

References


[1] Alan W. Bierman, "An Overview Course in Academic Computer Science: A New Approach for Teaching Nonmajors", The Proceedings of the Twenty-first SIGCSE Technical Symposium on Computer Science Education, Louisville, Kentucky, (March, 1990).

[2] Lynne V. Cheney, "50 Hours- A Core Curriculum for College Students", National Endowment for the Humanities, (October, 1989).

[5] C. Van Dyke, "Taking 'Computer Literacy' Literally", Comm. ACM, 30, 5, (May, 1987).

[3] J. Paul Myers, Jr., "The New Generation of Computer Literacy", The Proceedings of the Twentieth SIGCSE Technical Symposium on Computer Science Education, Louisville, Kentucky, (February, 1989).

[4] J. Paul Myers, Jr., "The Central Role of Mathematical Logic in Computer Science", The Proceedings of the Twenty-first SIGCSE Technical Symposium on Computer Science Education, Louisville, Kentucky, (March, 1990).

[5] C. Van Dyke, "Taking 'Computer Literacy' Literally", Comm. ACM, 30, 5, (May, 1987).

[6] The National Commission on Excellence in Education, A Nation at Risk: The Imperative of Educational Reform, U.S. Government Printing Office (1983).

[7] National Research Council, Everybody Counts: A Report to the Nation on the Future of Mathematics Education, National Academy Press (1989).

[8] Phyllis Keller, Getting at the Core: Curricular Reform at Harvard, Harvard University Press (1982).

[9] William Dunham, A 'Great Theorems' Course in Mathematics, American Mathematical Monthly (Dec. 1986).

[10] Alan Bierman, Great Ideas in Computer Science, MIT Press (1990).

[11] Evelyn Raskin and David R. Owen, Evaluation of the Core Curriculum, Brooklyn College of the City University of New York (1988).

[12] Undergraduate Science, Mathematics and Engineering Education, National Science Board, Pub. No. NSB 86-100 (1986).

[13] Report on the NSF Disciplinary Workshops on Undergraduate Education, National Science Foundation, Pub. No. NSF 89-3 (1989).

[14] Report on the NSF Workshop on Undergraduate Science, Engineering and Mathematics Education in Two Year Colleges, National Science Foundation, Pub. No. NSF 89-50 (1989).

[15] Albert Y. Pang and William A. Malmgren, Experiments in Logic and Computer Design, Prentice-Hall (1984).

[16] John Passafiume and Michael Douglas, Digital Logic Design: Tutorials and Laboratory Exercises, Harper and Row (1985).

[17] David Arnow, The Iliad and the WHILE Loop, SIGCSE (1991).

[18] Jean Buddington Martin and Kenneth E. Martin, A Profile of Today's Computer Literacy Students: An Update, The Proceedings of the Nineteenth SIGCSE Technical Symposium on Computer Science Education, (February, 1989).

[19] Antony Halaris and Lynda Sloan, Towards a Definition of Computing Literacy for the Liberal Arts Environment, The Proceedings of the Fifteenth SIGCSE Technical Symposium on Computer Science Education, (February, 1985).

[20] Shiela Tobias, They're Not Dumb, They're Different: a New Tier of Talent for Science, Change 22, 4 (1990).

[21] David Gries and Dorothy Marsh, The 1989 Taulbee Report, Comm. ACM, 33, 9, (Sept., 1990).

Back to David Arnow's CS Education Page.




tc