CSci 550: Program Semantics and Derivation
Fall Semester 1996
Syllabus

Locations

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 p.m.to 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)

Prerequisites

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

Source Materials

Textbook:

Edward Cohen. Programming in the 1990's. Springer-Verlag, 1990.

Report:

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.

Report:

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.

Readings:

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

Assignments

• All students are expected to study the relevant portions of the textbook and handouts in conjunction with our class discussions. Explicit reading assignments will not always be given.
• No required (on-machine) programming assignments are planned.
• Homework problem sets will be assigned periodically (e.g., weekly); approximately one week will be allowed for completion of each assignment.
• All students are expected to do their own work on homework assignments.
• All students are expected to complete their homework assignments by their due dates. Late homework papers will be accepted for up to one week after the due date, but grade penalties will increase daily.

Examinations

• Three equally weighted examinations
• Third examination will be given during final examination period
• Each exam will cover all topics studied to that point
• Each exam may consist of a combination of in-class and take-home components

Grading

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 ]