CSCI 550 (Program Semantics/Derivation) Spring 2006 Syllabus (Mississippi)

CSci 550: Program Semantics and Derivation
Spring Semester 2006
Syllabus


Locations

The spring semester 2006 class meets in Weir Hall 235 from 8:00 a.m. until 9:15 a.m. on Tuesdays and Thursdays.

The class is taught by Prof. Conrad Cunningham, whose office is 203 Weir Hall. Prof. Cunningham’s official office hours for this semester are 10:00 a.m. until 11:30 a.m. on Monday and Wednesday by appointment at other times.

Prof. Cunningham’s voice telephone number is (662) 915-5358 and fax number is (662) 915-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 Tuesday, 9 May.


Student Disabilities Services Statement

“It is the responsibility of any student with a disability who requests a reasonable accommodation to contact the Office of Disability Services (915-7128). Contact will then be made by that office through the student to the instructor of this class. The instructor will then be happy to work with the student so that a reasonable accommodation of any disability can be made.”


Course Goals

Upon completion of this course, the student will be able to specify simple programs formally and prove them correct. The student will understand predicate logic and guarded command semantics. The student should also be able to apply basic program derivation techniques.


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:

David Gries. The Science of Programming. Springer Verlag 1981.

Reference book:

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. Reprinted January 2006. [ PDF]

Report:

H. C. Cunningham. Feijen’s Table of Cubes Problem. Technical Report UMCIS-1994-02, March 1994, Revised August 1996. Reprinted Janaury 2006. [ PDF]

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.


Professional Conduct

As a student in Csci 550, you are expected to conduct yourself in a professional manner according to the Honor Code of the School of Engineering, the Information Technology Appropriate Use Policy, the M Book, and any other relevant policies.

Limited Collaboration Policy. Unless otherwise indicated, any homework assignment or programming exercise given in this class will be an individual assignment. The work you submit is to reflect the knowledge, understanding, and skill that you have attained as an individual. However, the instructor does want to encourage the development of a community of scholars who are actively engaged in discussion of the ideas related to this course. With this in mind, you are allowed to discuss solutions of the homework and programming problems with other students if done so according to the following guidelines:


Assignments


Examinations


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]


Send any comments or suggestions to Prof. Conrad Cunningham, cunningham@cs.olemiss.edu.
Copyright &copy 2006, H. Conrad Cunningham
Last modified: 16 Jan 2006.