Homework & Grades
Old Homework Directory
Q & A
U. of Iowa Homepage
About Computer Science 181
This page provides general information about the Spring 2001 offering of Computer Science 181 at the University of Iowa. This page is organized as follows:
Lecture attendance is required. The Meeting time and location is as follows:
There is one required text for the course, Edward Cohen's Programming in the 1990s: An Introduction to the Calculation of Programs (Springer-Verlag, 1990, ISBN 0-387-97382-6).
You can get a copy of this book as a course packet from the University Bookstore. (The book is out of print, so we have permission from Springer-Verlag to make copies; part of the cost of the copy is a royalty to Springer-Verlag.) There may also be some used copies of the printed book available at the bookstores.
We will supplement the text with other material as described in the syllabus's bibliography.
You must have an account on the department Unix machines.
We would like to hear from you if you have a disability that may require some modification of seating, testing, or other class requirements. If so, please talk to Gary Leavens as soon as possible so appropriate arrangements may be made.
From the Univ. of Iowa Catalog: "Models, methods and their application in all phases of software engineering process; operational, algebraic, model-based, property-based specification methods; verification of consistency, completeness of specifications; verification of software properties; exercises in specification construction, verification using method-based tools. Prerequisite: grade of C- or higher in 22C:180. Same as 055:181."
A formal method applies mathematical techniques to the problems of producing computer systems. According to Hinchey and Bowen (in the article "Applications of Formal Methods FAQ," chapter 1 of their book Applications of Formal Methods, Prentice-Hall, 1995, page 1.) "a formal method is a set of tools and notations (with a formal semantics) used to specify unambiguously the requirements of a computer system that supports the proof of properties of that specification and proofs of correctness of an eventual implementation with respect to that specification."
A model is a mathematical abstraction. A method is a description of a particular software process, including tools, notations, and other forms of guidance. An operational method is one that uses the execution of some program as a description of intended behavior; for example, one might want to program an editor that acts just like Microsoft Word. An algebraic method is one that uses compositions of the system's operations to describe its intended behavior. A model-based method is one that uses a mathematical model in stating properties of the system's intended behavior. A property-based method is one that uses properties expressed in some way other than algebraic or model-based techniques (e.g., using temporal logic). Such descriptions are called the specifications. Verification means mathematical proof that some property holds; for example, one can verify the correctness of an implementation with respect to a specification. Consistency holds when there are no internal contradictions; completeness holds when nothing relevant has been left out of a mathematical description.
Focus of this offering
We will focus the course to achieve some more depth than would be possible with a survey. We hope that this will give you more experience which will help you evaluate the advantages and disadvantages of formal methods.
This offering of the course will focus primarily on construction of specifications using model-based techniques, evaluation of the "goodness" of such specifications (including the notions of consistency and completeness, among others), and verification of software properties. We will show how to construct an implementation that automatically satisfies its specification. Furthermore, because the prerequisite course (180) focused on requirements and analysis, we will focus more on later phases of the software process. To make the material more concrete and applicable, we will discuss how it relates to sequential, object-oriented software. In particular, we will apply the ideas to Java, using the specification language JML.
Time permitting, we will also deal with the design of JML, and extending it to encompass some features necessary for modeling concurrent and reactive systems.
The general objectives for this course are divided into two parts: a set of essential objectives, and a set of enrichment objectives. The essential objectives will be helpful for your career as a computer scientist or software engineer; hence we want to help you to master them. You are encouraged to explore the enrichment objectives both for their own sake and because learning more about those will help deepen your understanding of the essential objectives.
In one sentence, the main objective is that you will have a deep, working knowledge of how to specify and verify sequential, object-oriented Java classes and interfaces. In more detail the essential objectives for this course are that you will be able to:
You will be permitted to use the textbook and course notes for tasks involving specification, verification, and programming, but some exams may limit your access to such resources.
There are two unusual features in the above objectives. The first is the use of Java and JML. One motivation for this is to focus the material; as explained above. Another is that I think it will be more interesting and exciting to have you involved in my research work.
The second unusual feature is the use of calculational style proofs and derivations. This style has been advocated by Dijkstra, Gries, and their followers as a way to help ensure that no mistakes are made in program proofs. I have found that the discipline of developing proofs without "pulling any rabbits out of the hat" is an admirable way of teaching, learning, and seeking precision.
Enrichment objectives could be multiplied without limit, but the following seem most important or most likely to be taught.
The formal prerequisites in the U. of Iowa catalog are a C- or higher grade in 22C:180 (Fundamentals of Software Engineering).
Many thanks to Curtis Clifton at Iowa State for his initial work on the HTML for these web pages, which I have adapted from another course.
Last modified Thursday, June 25, 2009.
This web page is for the Spring 2001 offering of 22C:181 at the University of Iowa. The details of this course are subject to change as experience dictates. You will be informed of any changes. Thanks to Curt Clifton for help with an earlier version of these web pages. Please direct any comments or questions to Gary Leavens.