The Department of Computer Science & Engineering 
CSE 451: PROGRAM DEVELOPMENT  Fall 1999

CLASS  INSTRUCTOR  REGIS. NO.  DAYS  HOURS  LOCATION 

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 
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.In addition, you will also have an opportunity to read some of the classic literature on program development and program verification.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 handinhand, 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]:
 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.
 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.
 Programming as a goaloriented developmental activity, based on the formal definition of a small language.
 Developing ... procedures ... and proving calls on them correct. ...
 Documenting programs in Pascal and other languages in light of correctnessproof principles.
 Inverting programs.
 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.
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.
Homework  24% 
MidSemester Exam I  24% 
MidSemester Exam II  24% 
Final Exam  24% 
Term Paper  4% 
Total  100% 
Tuesday  August 31  First Lecture 
Tuesday  September 21  Follow Monday schedule! 
Tuesday  September 28  MIDSEMESTER EXAM I 
Friday  October 22  Last day to withdraw with grade of "R" 
Thursday  November 4  MIDSEMESTER EXAM II 
Wed.Sun.  November 2426  Thanksgiving recess 
Thursday  December 9  Last lecture 
Mon.Mon.  December 1320  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.11.3  Propositional Logic:
propositions & their evaluation 
Th, Sep 2 
Sects. 1.32.1  operators, tautologies, translation, laws of equivalence  T, Sep 7 
Sects. 2.12.3  substitution, transitivity, formal systems  Th, Sep 9 
Sects. 4.14.3  Predicate Logic:
states, quantification, identifiers 
T, Sep 14 
Sects. 4.34.6  substitution, quantification  Th, Sep 16 
review for exam  Th, Sep 23  
MIDSEMESTER EXAM I  T, Sep 28  
review of exam  Th, Sep 30  
pp. 312313;
Sects. 5.15.2 
Program Syntax:
sequences, arrays 
T, Oct 5 
Sects. 5.36.3  arrays of arrays, program specifications,
variables, proof outlines 
Th, Oct 7 
Chs. 78  Program Semantics:
weakest precondition, skip, abort, composition 
T, Oct 12 
Sects. 9.19.2, 9.4  assignment statement  Th, Oct 14 
Chs. 1011  ifthenelse, while loops  T, Oct 19 
Ch. 11  while loops (cont'd.)  Th, Oct 21 
Sects. 12.112.2  procedure calls  T, Oct 26 
Sects. 12.312.4  procedure calls (cont'd.)  Th, Oct 28 
review for exam  T, Nov 2  
MIDSEMESTER EXAM II  Th, Nov 4  
review of exam  T, Nov 9  
Chs. 1314  Program Development:
Introduction 
Th, Nov 11 
Ch. 14; Sect. 15.1  loop guards  T, Nov 16 
Sects. 15.115.2  loops  Th, Nov 18 
Sects. 16.116.3  loop invariants  T, Nov 23 
Sects. 16.316.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 