CSci 550: Program Semantics and Derivation
Spring Semester 1998
Syllabus

Locations

The spring semester 1998 class meets in Weir Hall 351 from 9:30 a.m. until 10:45 on 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 10:00 a.m. until Noon on Monday and Wednesday by appointment at other times.

Prof. Cunningham's voice telephone number is (601) 232-5358 and fax number is (601) 232-5623. His WWW home page is http://www.cs.olemiss.edu/~hcc/ and his email address is cunningham@cs.olemiss.edu (send).

The WWW home page for this class is http://www.cs.olemiss.edu/~hcc/csci550/.

The final examination for this class is scheduled at 8:00 a.m. on Thursday, 7 May.

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, HP PCL, 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, HP PCL, 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

All students in CSCI 550 are expected to conduct themselves according to the Honor Code of the School of Engineering at the University of Mississippi:

"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 unless the assignment is explicitly specified as a group project.
• All students are expected to complete their homework assignments by their due dates. (Late homework papers might be accepted for a few days after the due date, but grade penalties will increase daily. No homework will be accepted after the final examination period.)

Examinations

• There will be three examinations; the third examination is optional for those persons who have a grade of "A" going into the final examination.
• The examination portion of the semester grade will be calculated by averaging the two best examination grades.
• The first examination will be given in late February or early March.
• The second examination will be given in mid-April.
• The third examination will be given during the final examination period. (Students who opt not to take the final examination may be given an assignment that is due during finals week.)
• Each exam will cover all topics studied to that point.
• Each exam may consist of a combination of in-class and take-home components.
• If you cannot take an examination at the scheduled time because of an illness or other special circumstances, please notify Prof. Cunningham in advance. Without advance notification, it may not be possible to give a make-up examination.
• Please do not ask to take the final examination earlier than the time set for the entire class.

Grading

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

Two-thirds of the semester grade will come from the exam average and one-third from the homework assignment average.

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