The Department of Computer Science & Engineering


(Available on the Web at:
(Other relevant links: CSE 451 homepage, Directory of Documents, newsgroup, newsgroup archive.)

8 September 1999
NEW material is highlighted


CSE 116 and some formal logic (e.g., as currently taught in CSE/MTH 191-192 or MTH 314). (The official prerequisite of CSE 305 would be helpful but is not strictly necessary.)


Dr. William J. Rapaport, 214 Bell Hall, 645-3180 x 112,

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


Lecture Rapaport 306065 TTh 11:00 a.m. - 12:20 p.m. Capen 260
Recitation R1 no one 167340 M 4:00 p.m. - 4:50 p.m. Norton 209
NOTE: Recitations will ***NOT*** meet!!
But the room might be available (until further notice) for your use.



The official catalog description says:
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.
David Gries, the author of our text says:
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.
In addition, you will also have an opportunity to read some of the classic literature on program development and program verification.


  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).


  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".


  1. Homework assignments will be of the "paper-and-pencil" variety, to be done at home.
  2. The purposes of homeworks are:
  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:

    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.

  6. 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.
  7. 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. 
  8. 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.


All graded work will receive a letter grade, 'A', 'A-', 'B+', 'B', 'B-', 'C+', 'C', 'C-', 'D+', 'D', or 'F'. Your course grade will be calculated as a weighted average of all letter grades according to the following weights:
Homework 24%
Mid-Semester Exam I 24%
Mid-Semester Exam II 24%
Final Exam 24%
Term Paper 4%
Total 100%


It is University policy that a grade of Incomplete is to be given only when a small amount of work or a single exam is missed due to circumstances beyond the student's control, and that student is otherwise doing passing work. I will follow this policy strictly! Thus, you should assume that I will not give incompletes :-) Any incompletes that I might give, in a lapse of judgment :-), will have to be made up by the end of the Spring 2000 semester. For more information on Incomplete policies, see the web page, "Incompletes".


Tuesday  August 31 First Lecture
TuesdaySeptember 21Follow Monday schedule!
Tuesday September 28 MID-SEMESTER EXAM I
Friday October 22 Last day to withdraw with grade of "R"
Thursday November 4 MID-SEMESTER EXAM II
Wed.-Sun. November 24-26 Thanksgiving recess
Thursday December 9 Last lecture
Mon.-Mon. December 13-20 Exam Week
Assume our exam is the afternoon of the last day!


Sections Topics Lecture Dates
Preface Intro to course:
program verification & program development 
T, Aug 31
Part 0; Sects. 1.1-1.3  Propositional Logic:
propositions & their evaluation
Th, Sep 2
Sects. 1.3-2.1  operators, tautologies, translation, laws of equivalence T, Sep 7
Sects. 2.1-2.3  substitution, transitivity, formal systems Th, Sep 9
Sects. 4.1-4.3  Predicate Logic:
states, quantification, identifiers
T, Sep 14
Sects. 4.3-4.6  substitution, quantification Th, Sep 16
review for exam Th, Sep 23
review of exam Th, Sep 30
pp. 312-313;
Sects. 5.1-5.2
Program Syntax:
sequences, arrays 
T, Oct 5
Sects. 5.3-6.3  arrays of arrays, program specifications,
variables, proof outlines
Th, Oct 7
Chs. 7-8  Program Semantics:
weakest precondition, skip, abort, composition
T, Oct 12
Sects. 9.1-9.2, 9.4  assignment statement Th, Oct 14
Chs. 10-11  if-then-else, while loops T, Oct 19
Ch. 11  while loops (cont'd.) Th, Oct 21
Sects. 12.1-12.2  procedure calls T, Oct 26
Sects. 12.3-12.4  procedure calls (cont'd.) Th, Oct 28
review for exam T, Nov 2
review of exam T, Nov 9
Chs. 13-14  Program Development:
Th, Nov 11
Ch. 14; Sect. 15.1  loop guards T, Nov 16
Sects. 15.1-15.2  loops Th, Nov 18
Sects. 16.1-16.3  loop invariants T, Nov 23
Sects. 16.3-16.5  loop invariants (cont'd.) T, Nov 30
Sect. 16.5  loop invariants (cont'd.) Th, Dec 2
Ch. 21  inverting programs T, Dec 7
summary of course Th, Dec 9


While it is acceptable to discuss general approaches with your fellow students, the work you turn in must be your own. If the work of two or more students appears unjustifiably similar, penalties (ranging from an F in the assignment to an F in the course) will be assessed to all concerned. If you have any problems doing the homeworks or projects, consult the TA or Prof. Rapaport. Also see the webpage, "Academic Integrity"

William J. Rapaport (
file: 451/syl.08sp99.html