Com S 641/Refinement Calculus Seminar

About Com S 641

This page provides general information about the Spring 2002 offering of Computer Science 641 at Iowa State University. This page is organized as follows:

1. Meetings
2. Course Textbooks
3. Computer Accounts
4. Course Description
5. Objectives
6. Prerequisites
7. Acknowledgments

Meetings

Lecture attendance is required. The Meeting time and location is as follows:

Lectures
Mondays, Wednesdays, Fridays
4:10-5:00pm, 214 Atanasoff Hall

Return to top

Course Textbooks

There 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.

Return to top

Course Description

From the Iowa State Catalog: "Operational and other mathematical models of programming language semantics. Type systems and their soundness. Application of semantics to program correctness, language design and translation. (3 credits)"

Some Explanation

A model is a mathematical abstraction. Operational models of programming languages are exemplified by Plotkin's terminal transition systems (rewrite rules) or Landin's SECD machine (an interpreter). Rewrite rules are closely related to logics and deductive systems, although these are not usually considered models at all, but the foundations of proof theory. Other kinds of mathematical models include the denotational models, exemplified by the Scott-Strachey approach, which uses functions over various domains. Another approach to describing semantics is more axiomatic, such as Hoare logics, which can be used to describe partial correctness of imperative programs, and inference systems used in the study of ``logic-oriented'' languages (such as Prolog) or type theory.

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 offering

This 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.

Return to top

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 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 Objectives

Enrichment 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.

Return to top

Prerequisites

The 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.

Return to top

Acknowledgments

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.

Return to top

Last modified Tuesday, January 22, 2002.