General Info.
Course Homepage
About 22C:181
Contacting Us
Syllabus
Homework & Grades
Grading Policies
Grades
Old Homework Directory
Old Exams
Reference
Q & A
Meeting outlines
Resources
JML
Links
FM Links
Department Homepage
U. of Iowa Homepage
Course Syllabus
The table below gives the planned syllabus for the course. This syllabus is subject to change. If it becomes necessary to revise the schedule, then this page will be updated to reflect the changes.
The references in the readings are given in the bibliography below.
| Dates | Topics | Readings | Optional Readings |
|---|---|---|---|
| Jan. 16 | Introduction | Handouts, Course Web Site | |
| Jan. 16-Feb. 1 | Overview of Formal Methods | [Wing90] | [Hinchey-Bowen95], Formal Methods Virtual Library |
| Jan. 18 | Guest Matt Wilding talks about "Executable Formal models" | ||
| Jan. 25 | Guest Steve Miller talks about formal methods at Rockwell | ||
| Feb. 1-Feb. 8 | Calculation and Precision | [Cohen90] Ch. 0, 1 | [Dijkstra76] [Gries91] |
| Feb. 8-Feb. 20 | Predicates | [Cohen90] Ch. 2, 3 | [Dijkstra-Scholten90] |
| Feb. 22-Feb. 27 | Program Development | [Cohen90] Ch. 4-5 | |
| Mar. 1 | Exam I | [Wing90], [Cohen90] Ch. 1-3 | Formal Methods Virtual Library, [Dijkstra-Scholten90] [Dijkstra76] |
| Mar. 6 | Program Development | [Cohen90] Ch. 4-5 | |
| Mar. 8 | Program Development | [Cohen90] Ch. 6-7 | |
| Mar. 13-Mar. 15 | Spring Break, no class | ||
| Mar. 22 | Program Development | [Cohen90] Ch. 6-7 | |
| Mar 27.-Mar. 29 | Loops | [Cohen90] Ch. 8-9 | |
| Apr. 3 | Exam review | [Cohen90] Ch. 4-9 | |
| Apr. 5 | Exam II | [Cohen90] Ch. 4-9 | |
| Apr. 10, Apr. 17 | Loops | [Cohen90] Ch. 10 | |
| Apr. 12 | Recursion | [Cohen90] Ch. 11 | |
| Apr. 12, Apr. 19-Apr. 24 | JML Intro. | [Leavens-Baker-Ruby01] | JML web page, [Cohen90] Ch. 12 |
| Apr. 26-May 3 | Data Abstraction | [Hoare72] | [Liskov01] Ch. 5 |
| May 3 | Summary and Evaluation | ||
| Tues., May 8, 7-9 p.m. | Final Exam | [Cohen90] Ch. 10-12, [Leavens-Baker-Ruby01] | JML web page, [Liskov01] Ch. 5 |
Bibliography
- [Cohen90]
- Edward Cohen. Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, New York, N.Y., 1990.
- [Dijkstra-Scholten90]
- Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and program semantics. Springer-Verlag, New York, N.Y., 1990.
- [Dijkstra76]
- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.
- [Hinchey-Bowen95]
- Michael G. Hinchey and Jonathan P. Bowen. Applications of Formal Methods FAQ. In Michael G. Hinchey and Jonathan P. Bowen (eds.), Applications of Formal Methods, pp. 1-15, Prentice Hall, London, 1995.
- [Hoare72]
- C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271-281 (1972).
- [Gries91]
- David Gries. Teaching Calculation and Discrimination: A More Effective Curriculum. Comm. ACM, 34(3):44-55 (March, 1991).
- [Leavens-Baker-Ruby01]
- Gary T. Leavens, and Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Iowa State University, Department of Computer Science, TR98-06n, June 1998, revised July, November 1998, January, April, June, July, August, December 1999, February, May, July, December 2000, February, April 2001. [Postscript] [PDF]
- [Liskov01]
- Barbara Liskov with John Guttag. Program Development in Java. Addison-Wesley, Boston, Mass, 2001.
- [Wing90]
- Jeannette M. Wing. A Specifier's Introduction to Formal Methods. Computer, 23(9):8-24 (Sept. 1990).
Course Content and Policies
The course's content and grading polices are described on separate web pages. See the links on the top left of this page.
Last modified Tuesday, May 8, 2001.