Course Information

There is also a class afs directory: /afs/cs/academic/class/15671-f97. It will contain various templates and documents that can be helpful in completing your homework.

Communication. We have set up three mechanisms for out-of-class interaction.

1. The Course Bulletin Board. We will use cmu.cs.class.cs671 to post questions/answers about homework and lectures. So you should plan to read it regularly. Feel free to use it yourself to post about topics of general interest for the other students.

2. Office Hours: The instructor and the TA has weekly office hours, listed above.

3. Email: We welcome email about the course at any time.

Readings. Most lectures will have a reading assignment that we expect you to complete before you come to class. Many of the reading assignments will be drawn from the the required textbook for the course: An Introduction to Formal Specification and Z, by Potter, Sinclair, Till [PST]. Additionally, the course has an optional reference book: The Z Notation: A Reference Manual, Second Edition, by J. M. Spivey. Some readings are in the form of handouts to supplement some lectures; other additional readings are technical papers. These will be distributed as needed throughout the course.
Finally, there a number of additional books that will be put on reserve. These are noted in References at the end of this document.

Homeworks and Lab Exercises. The course is organized around (roughly) weekly homeworks. The purpose of the assignments is to give you practice in using the models and logics of the course. In some cases where a model is supported by tools we may also assign one or more ungraded lab exercises. These are intended to give you practice in using the tools before you have to apply them on the homework problems. We encourage you to discuss your homework with other students, but the final write-up must be your own work.

Homeworks will be graded on a pass/fail basis. Occasionally, we will take special note of a homework that is exceptionally well done. Homework assignments will typically be assigned on a Monday and due at the beginning of class a week later. To give you the most opportunities to learn from the homework assignments, we will allow you to redo a homework that didn't receive a passing grade. A redone homework must be turned in at the class following the one on which it is handed back.

Extra copies of handout materials. Extra copies of lecture slides, handouts, homework assignments, etc. will be available from Heather Marko, WeH 8120 and in the shelves next to the door to WeH 4615.

Exams. There will be a (take-home) mid-term (handed out October 11, due October 13) and a (in-class) final examination.

Homework Presentations. For some homework assignments we will ask students to present their results on the day it is due. The purpose of this is to give the presenter practice at explaining a solution to others and to give the rest of the class a chance to see how someone else solved the problem. These presentations will be assigned on a rotating basis, as necessary and will be ungraded.

Grading. The course grade will be determined as a combination of four factors: homework exercises (50%), midterm exam (15%) final exam (25%), instructorsí judgment (10%).

(Go to the current version of the syllabus with links)

Schedule

Bold refers to PST

* marks classes that follow a holiday

References