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
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:
- Meetings
- Course Textbooks
- Computer Accounts
- Accomodations for Disabilities
- Course Description
- Objectives
- Prerequisites
- Acknowledgements
Meetings
Lecture attendance is required. The Meeting time and location is as follows:
Lectures
Tuesdays, Thursdays
2:30-3:45pm, 114 MLH
Course Textbooks
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.
The texts, plus some additional resources, will be on reserve at the Mathematical Sciences library. The library is in the process of ordering the text.
We will supplement the text with other material as described in the syllabus's bibliography.
Computer Accounts
You must have an account on the department Unix machines.
Accomodations for Disabilities
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.
Course Description
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."
Some Explanation
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.
Objectives
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.
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:
- Explain when and why one should use formal methods, and their advantages, disadvantages, and limits.
- Explain how specification and verification relate to design, coding, and testing.
- Design procedures and abstract data types at an appropriate level of abstraction that permits multiple, different implementations.
- Explain design alternatives for dealing with aliasing, and exception handling, and how they relate to specification and verification.
- Write formal specifications (written in JML) for sequential (Java) classes and interfaces. These will be based on either informal requirements or existing code.
- Inspect formal specifications for consistency, completeness, abstraction level, and other qualities.
- Calculate correct sequential (Java) code from (JML) specifications.
- Inspect proofs of correctness for (Java) code.
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
Enrichment objectives could be multiplied without limit, but the following seem most important or most likely to be taught.
- Be proficient at detecting ambiguity in English or other kinds of informal specifications.
- Explain how to design and document object-oriented frameworks or class libraries that are intended for subclassing.
- Explain what the specification and verification techniques are appropriate for each kind of software.
- Explain the economic costs and benefits of using various kinds of formal methods for various kinds of software.
- Use formal specifications to evaluate the quality of a design.
- Explain what kinds of problems can be tackled automatically by tools, and what does tools are capable of doing.
- Explain the language constructs that aid in various kinds of specification, and how they help.
- Explain the research and scientific questions that are open in the area of formal methods.
Prerequisites
The formal prerequisites in the U. of Iowa catalog are a C- or higher grade in 22C:180 (Fundamentals of Software Engineering).
Acknowledgements
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.