UNIVERSITY AT BUFFALO - STATE UNIVERSITY OF NEW YORK
The Department of Computer Science & Engineering

CSE 451: PROGRAM DEVELOPMENT - Fall 1999

material is highlighted

PREREQUISITE:

PROFESSOR:

Dr. William J. Rapaport, 214 Bell Hall, 645-3180 x 112, rapaport@cse.buffalo.edu

Office Hours: Mondays, 2:00-3:00 p.m.; Fridays, 10:00-11:00 a.m.; and by appointment.

CLASS MEETINGS:

TEXT:

• Gries, David (1981), The Science of Programming, 3rd printing or later (1985) (New York: Springer-Verlag); ISBN 0-387-90641-X (cloth), 0-387-96480-0 (paper).
• In addition, there are several items on reserve at UGL/SEL, in particular:
• Colburn, Timothy R.; Fetzer, James H.; & Rankin, Terry L. (eds.) (1993), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers).

DESCRIPTION OF COURSE:

Introduction to the simultaneous development and verification of correct programs. In preparation for this, the first part of the course will contain lectures in formal logic and in program semantics. The second part will involve actual examples of program development.

The practical development of correct programs based on the conscious application of principles that are derived from a mathematical notion of program correctness. Programs are written but not run on a computer.

The goal of the course is to teach ideas on "programming methodology" that have been developed in the past fifteen years. The ideas are based on defining a programming language (or part of one) in terms of proving programs correct and developing proof and program hand-in-hand, using the principles and techniques derived from the theory of correctness. A kind of calculational style of programming emerges, where at each step some calculation, some manipulation of program or predicates, provides the next step in the derivation of the program.

The methods are meant to be practical --and fun. There will be no need in this course to test programs on the computer. Rather, the goal is to learn to understand and develop programs in such a fashion that we know the programs are correct. This requires a change in thoughts and habits. Look upon this course as an experiment in thinking --can you actually learn how to think differently, more effectively, about the development of programs? Can the use of formalism really help? The emphasis on method, on the conscious application of principles, on formal development, and on the continual search for mathematical simplicity and elegance may make the course different from ones you have previously had.

After the course, you may choose to abandon completely what you have learned in this course and return to your old habits. But, during this course, when developing each and every program, take part in the experiment and consciously follow the methods prescribed to the best of your ability.

Topics of the course [as Gries teaches it]:

1. The use of logic --a predicate calculus. Logic is the backbone of the theory and practice of programming. The use of formal manipulation in developing programs is an important part of the programming methodology. We will spend some time making sure that you understand the basic notions of logic and have a facility, an agility, in manipulating formulas.
2. The specification of programs using Hoare triples and Dijkstra's weakest preconditions. The definition of a small imperative language: assignment, sequencing, a conditional statement, and a loop.
3. Programming as a goal-oriented developmental activity, based on the formal definition of a small language.
4. Developing ... procedures ... and proving calls on them correct. ...
5. Documenting programs in Pascal and other languages in light of correctness-proof principles.
6. Inverting programs.
7. Algorithms. In the course, you will derive or see derived over 50 algorithms using the methodology to be taught, some quite complex. Many of these will be basic computer science algorithms in standard areas of concern, so the course will enlarge your algorithmic horizon as well as teach you a useful programming methodology.

ATTENDANCE, HOMEWORKS, AND EXAMS:

1. You will be expected to attend all lectures and to complete all readings and assignments on time. There will be regular homework assignments, two mid-semester exams, a comprehensive final exam (during exam week), and a brief (2 - 5-page) term paper on one (or more) of the classic papers in the field. Taking all the exams is a necessary condition for passing the course. Writing the term paper is a necessary condition for getting an A in the course. No programming will be required.
2. All homeworks will be announced in lecture. Therefore, be sure to get a classmate's phone number (for instance, 1 or 2 people sitting next to you in class, whoever they are!), so that you will not miss assignments in the unlikely event that you miss a class.
3. From time to time, information about homeworks, etc., will be posted to the newsgroup sunyab.cse.451, which you should read on a regular basis.
4. Students should notify the instructor within the first two weeks of class if they have a disability which would make it difficult to carry out course work as outlined (requiring note-takers, readers, extended test time).

READING AND STUDYING:

1. I strongly urge you to read all of the text, including those sections that we do not cover in the course.
2. Not all assigned readings will be covered in lecture (in lecture, we will only cover interesting or hard material, plus occasionally material that is not in the text), but you are responsible for all assigned material in the text and lectures.
3. See "How to Read (a Computer Science Text)".
4. For general advice on how to study for any course, see my web page, "How to Study".

HOMEWORKS:

1. Homework assignments will be of the "paper-and-pencil" variety, to be done at home.
2. The purposes of homeworks are:
• to give you practice in applying the concepts covered in the course
• to give you a chance to assess the level of your understanding
3. There will be approximately 1 HW each week.
4. Due dates will be announced in lecture when the homework is assigned. HWs will be collected at the start of lecture on the due date. If you try to hand yours in after they have been collected (e.g., at the end of lecture, in my mailbox, etc.), it will not be accepted. To repeat:
NO LATE HOMEWORKS WILL BE ACCEPTED.

This is so that the homework can be discussed in the class period when it is due and so that I can hand out answers on the day the homework is due.

5. Put your full name and date at the top right-hand side of the each page, and secure all pages with a staple in the top left-hand corner.
6. Note: The lowest homework grade will be dropped; you should assume that you will fail to turn in one homework (oversleep, get stuck in traffic, etc.)--that's the one that will be dropped. If you know now that you will regularly be late, see me to make alternative arrangements for turning in your work. Your graded HW will be returned in lecture. 
7. Just as you cannot expect to learn how to drive a car by reading about it or by watching other people do it, the same holds true for doing computer science. Do your work on time--this is one course you simply cannot cram for at the last minute, so don't even try! I cannot stress this strongly enough. Remember that the homeworks may be fairly time-consuming, so please consider your other commitments, and plan your time accordingly.

GRADING:

Incompletes:

IMPORTANT DATES:

TENTATIVE SCHEDULE:

ACADEMIC HONESTY: