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 ReferenceQ & A Old 641 Meeting outlines Resources JML LinksRefinement Calculus Java Formal Methods Department Homepage Iowa State U. Homepage |
## About Com S 641This page provides general information about the Spring 2002 offering of Computer Science 641 at Iowa State University. This page is organized as follows: - Meetings
- Course Textbooks
- Computer Accounts
- Course Description
- Objectives
- Prerequisites
- Acknowledgments
## MeetingsLecture attendance is required. The Meeting time and location is as follows:
## Course TextbooksThere is one required text for the course, Ralph-Johan Back and Joakim von Wright's Refinement Calculus: A Systematic Introduction (Springer-Verlag, New York, 1998, ISBN 0-387-98417-8). The texts, plus some additional resources, will be on reserve at the Parks library. The course text is on order. We will supplement the text with other material as described in the syllabus's bibliography. ## Course Description
## Some ExplanationA Semantics and semantic models have many uses. One traditional use is as an aid to reasoning about the correctness of programs, or as a way to prove the soundness of such a reasoning system. Another use is in helping to design a language; the idea being that a language is well-designed if it has a simple and elegant semantics. Finally, one can use semantics to guide the construction of compilers and interpreters, or to prove that optimizations and program transformations are correctness-preserving. ## Focus of this offeringThis offering of the course will focus primarily on the refinement calculus, which is a specialized use of predicate transformer semantics; which are themselves a form of axiomatic semantics. The refinement calculus is an example of a wide-spectrum programming language: it includes constructs from both specification languages and programming languages. The idea is to start with an abstract specification, and then, through a series of small refinement steps, improve the program until it is executable and efficient. Each refinement step preserves correctness, so the series of refinement steps is essentially a proof that the final program correctly implements the abstract specification. Time permitting, we will also try to extend the ideas discussed in the class to object-oriented programming. In particular we may look at the design of JML, a behavioral interface specification language for Java. We will look into using the techniques of the refinement calculus to give a semantics to JML, and also to improving JML's support for the refinement calculus. You will also be encouraged to extend the techniques in other directions, for example, to component-based systems or to making computer systems more secure. ## ObjectivesThe 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 ObjectivesIn one sentence, the main objective is that you will be able to design a refinement calculus for a small programming language, to examine its quality using mathematical techniques, and to use it to design and prove correct small implementations of abstract specifications. We will focus on sequential programs, but allow nondeterminism. In more detail the essential objectives for this course are that you will be able to: - Explain the goals of the refinement calculus and how it can be used as a semantics for programming and specification languages, as well as its advantages, disadvantages, and limits.
- Use mathematical techniques to judge and improve the quality of refinement calculus definitions of programming languages.
- Explain and generalize the ideas behind the semantics of statements for sequential programs used in the refinement calculus.
- Use the refinement calculus to calculate correct implementations of abstract specifications.
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. We will use the calculational style proofs and derivations, as been advocated by Dijkstra, Gries, and their followers. This style is a discipline of developing proofs without "pulling any rabbits out of the hat". I find it is an admirable way of teaching, learning, and seeking precision. ## Enrichment ObjectivesEnrichment objectives could be multiplied without limit, but the following seem most important or most likely to be taught. Several of these relate to my research work on Java and JML. I think it will be interesting and exciting to have you involved in my research work. - Explain how to deal with advanced features like pointers or exception handling in the refinement calculus.
- Design an object-oriented refinement calculus, e.g., for a subset of Java or Smalltalk.
- Write formal specifications (written in JML) for sequential (Java) classes and interfaces. These will be based on either informal requirements or existing code.
- Calculate correct sequential (Java) code from (JML) specifications.
- Explain the language constructs that aid in various kinds of specification, and how they help.
- Explain how specification and verification relate to design, coding, and testing.
- Explain the research and scientific questions that are open in the area of refinement calculus, semantics of programming languages, and formal methods.
## PrerequisitesThe formal prerequisites in the Iowa State U. catalog are Com S 541 and Com S 531. For this offering of 641, the 531 prerequisite isn't so important. See the professor if you have questions about the prerequisites. ## AcknowledgmentsMany 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 Tuesday, January 22, 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.