Com S 641/Refinement Calculus Seminar

General Info.
Seminar Homepage
Seminar Syllabus
Homework Directory

Old 641 Homepage
About Com S 641
Contacting Us
Old 641 Syllabus
Old 641 Course Grading Policies
Old 641 Exams

Reference
Q & A
Old 641 Meeting outlines
Resources
JML

Links
Refinement Calculus
Java Formal Methods
Department Homepage
Iowa State U. 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. 14-18	No class (instructor away)	[BvW98] Ch. 1	[Morgan98] Ch. 1-7
Jan. 21	No class (University holiday)	[BvW98] Ch. 1	[Morgan98] Ch. 1-7
Jan. 23	Introduction	Handouts, Course Web Site
Jan. 23-Feb. 1	Overview	[BvW98] Ch. 1	[Morgan98] Ch. 1-7
Feb. 1-Feb. 4	Posets, Lattices, and Categories	[BvW98] Ch. 2	[Cohen90] Ch. 0-1 & 6, [Gries91]
Feb. 6-Feb. 11	Higher-Order Logic	[BvW98] Ch. 3	[Cohen90] Ch. 2-3, [Morgan98] Ch. 2, [Dijkstra-Scholten90]
Feb. 11-Feb. 15	Functions	[BvW98] Ch. 4	[Cohen90] Ch. 2-3, [Dijkstra-Scholten90]
Feb. 18-Mar. 1	States and State Transformers	[BvW98] Ch. 5	[Cohen90] Ch. 2-3, [Dijkstra76]
Mar. 1-15	Truth Values	[BvW98] Ch. 6
Mar. 18-Mar. 22	Spring Break, no class
Mar. 25	Review for Exam 1	[BvW98] Ch. 1-8	[Cohen90] Ch. 1-3 & 6, [Dijkstra-Scholten90], [Morgan98], Ch. 1-6
Mar. 27	Exam 1	[BvW98] Ch. 1-8	[Cohen90] Ch. 1-3 & 6, [Dijkstra-Scholten90], [Morgan98], Ch. 1-6
Mar. 29-Apr. 1	Predicates and Sets	[BvW98] Ch. 7
Apr. 3	Boolean Expressions and Conditionals	[BvW98] Ch. 8	[Cohen90] Ch. 2-3, [Morgan98] Ch. 2, [Dijkstra-Scholten90]
Apr. 3-15	Relations	[BvW98] Ch. 9	[Dijkstra-Scholten90]
Apr. 17-May 1	Predicate Transformers	[BvW98] Ch. 11	[Dijkstra-Scholten90]
May 3	Summary and Evaluation
Thurs., May 9, 2:15-4:15p.m.	Final Exam	[BvW98] Ch. 7-9, 11	[Cohen90] Ch. 2-3, [Morgan98] Ch. 2, [Dijkstra-Scholten90]

Return to top

Bibliography

[BvW98]: Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, New York, N.Y., 1998.
[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.
[Gries91]: David Gries. Teaching Calculation and Discrimination: A More Effective Curriculum. Comm. ACM, 34(3):44-55 (March, 1991).
[Morgan98]: Carroll Morgan. Programming from Specifications, Second Edition. Prentice-Hall International, 1998.
On-line at http://users.comlab.ox.ac.uk/carroll.morgan/PfS/.

Return to top

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.

Return to top

Last modified Monday, August 26, 2002.

This web page is for the Spring 2002 offering of Com S 641 or the Fall 2002 offering of Com S 610 GL at Iowa State University. The details of this course are subject to change as experience dictates. You will be informed of any changes. Please direct any comments or questions to Gary T. Leavens at leavens@cs-DOT-iastate-DOT-edu.