CSci 550: Program Semantics and Derivation
Fall Semester 1996


The fall semester 1996 class meets in Weir Hall 352 at 9:30 to 10:45 a.m., Tuesday and Thursday.

The class is taught by Prof. Conrad Cunningham, whose office is 312 Weir Hall. Prof. Cunningham's official office hours for this semester are 9:45 a.m. to 11:00 a.m. Monday & Wednesday, 1:15 2:30 p.m. Tuesday & Thursday, or by appointment.

The final examination for this class is scheduled at 4:00 p.m. on Wednesday, 11 December 1996.

Course Description from the Catalog

A study of formal methods for the specification, derivation, and verification of computer programs. Predicate logic; notations for specification of programs; programming language semantics; calculational techniques for the derivation of programs. (3 hours lecture)


Senior or graduate standing in computer science. (Previous study of introductory discrete mathematics, data structures, and algorithms is assumed.)

Source Materials

Edward Cohen. Programming in the 1990's. Springer-Verlag, 1990.
H. C. Cunningham. A Programmer's Introduction to Predicate Logic. Technical Report UMCIS-1994-02, February 1994, Revised January 1996. Available via anonymous FTP as Postscript or LaTeX dvi formats.
H. C. Cunningham. Feijen's Table of Cubes Problem. Technical Report UMCIS-1994-02, March 1994, Revised August 1996. Available via anonymous FTP as Postscript or LaTeX dvi formats.
Various journal and conference articles and research reports as appropriate.

Course Outline

  1. Introductory example.
  2. Predicate logic.
  3. Program specification techniques.
  4. Guarded Commands notation and its semantics.
  5. Program correctness verification.
  6. Program derivation techniques.

School of Engineering Honor Code Statement

"The Honor Code shall apply to all students, both undergraduate and graduate, registered in and/or seeking degrees through the School of Engineering. The Honor Code shall be understood to apply to all academic areas of the School such as examinations, quizzes, laboratory reports, themes, computer programs, homework, and other possible assignments. Only that work explicitly identified by the class instructor not to be under the Honor Code is excluded. The intent of the Honor Code is to recognize professional conduct and, thus, it shall be deemed a violation of the Honor Code to knowingly deceive, copy, paraphrase, or otherwise misrepresent your work in a manner inconsistent with professional conduct."




My grading scale is A [90..100], B [80..0), C [70..0), D [60..0), and F [0..60).

75% of the semester grade will come from the exam average and 25% from the homework assignment average.

[ CSci 550 Home ]
[ Cunningham's Home | Teaching ]
[ Department's Home | Courses | Undergraduate Courses | Graduate Courses ]

Send any comments or suggestions to Prof. Conrad Cunningham,
Copyright © 1996, H. Conrad Cunningham
Last modified: 21 August 1996.