The Department of Computer Science & Engineering
CSE 451: PROGRAM DEVELOPMENT - Fall 1999
|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 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]:
- 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 goal-oriented 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 correctness-proof 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.
|Mid-Semester Exam I||24%|
|Mid-Semester Exam II||24%|
|Tuesday||August 31||First Lecture|
|Tuesday||September 21||Follow 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!
|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|
|MID-SEMESTER EXAM I||T, Sep 28|
|review of exam||Th, Sep 30|
|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|
|MID-SEMESTER EXAM II||Th, Nov 4|
|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|