Old 641 Homepage
About Com S 641
Old 641 Syllabus
Old 641 Course Grading Policies
Old 641 Exams
Q & A
Old 641 Meeting outlines
Java Formal Methods
Iowa State U. Homepage
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:
Lecture attendance is required. The Meeting time and location is as follows:
We will supplement the text with other material as described in the syllabus's bibliography.
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)"
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.
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 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:
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 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.
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.
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 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.