About Computer Science 641

This page provides general information about the Spring 2006 offering of Computer Science 641 at Iowa State University. The course's home page is http://www.cs.iastate.edu/~cs641/. This page, which descibes the course is organized as follows:

  1. Meetings
  2. Course Textbooks
  3. Accommodations for Disabilities
  4. Course Description
  5. Objectives
  6. Prerequisites
  7. Acknowledgments

The course grading policy and syllabus are on separate web pages.

Information about previous offerings of this course is also available.

Meetings

Lectures

Attendance is required. These meetings are on Mondays, Wednesdays, and Fridays at 3:10-4:00pm in Sweeney 1120.

Return to top

Course Textbooks

There is one required text for the course.

Note that there is a second, corrected printing of this text published in 2005. It would be better to get the second printing. However, you can also get a list of corrections if you have the 1999 printing.

All the texts are on reserve at the Parks library.

We will supplement the text with other material as described in the syllabus.

Return to top

Accommodations 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 request that the Disability Resources staff send a SAAR (Student Academic Accommodation Request) form verifying your disability and specifying the accommodation you will need. Then bring the SAAR form along and talk to Gary Leavens as soon as possible so appropriate arrangements may be made.

Return to top

Course Description

From the Iowa State University Bulletin: "Operational and other mathematical models of programming language semantics. Type systems and their soundness. Application of semantics to program correctness, language design or 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 semester, we will focus on an exciting area in programming language semantics that intersects with formal methods and software engineering: program analysis. The textbook we will be using emphasizes the commonality between the different kinds of analysis, which include: data flow analysis, constraint-based analysis, abstract interpretation, and type and effect systems.

Time permitting, we will also try to extend the ideas discussed in the class to object-oriented programming. In particular we may look at how program analysis could be applied to JML, a behavioral interface specification language for Java. We will also try to explore counter-example guided abstraction refinement. 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. These objectives are linked to the course's learning outcomes (in references that look like this: [B3]). The essential objectives will be helpful for your career as a computer scientist; 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 program analysis [A1] [A2] [B3]. 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 both homework and tests.

Enrichment Objectives

Enrichment objectives could be multiplied without limit, but the following seem most important or most easily taught using the course text.

Return to top

Prerequisites

The formal prerequisites in the Iowa State U. catalog are Com S 541 and Com S 531. See Gary if you have questions about the prerequisites.

Return to top

Acknowledgements

Thanks to Samik Basu and John Hatcliff who suggested the textbook we are using this semester.

Many thanks to Curtis Clifton (now at Rose-Hulman) for his initial work on the HTML for these web pages, which I have adapted from another course.

Return to top

Last modified Friday, January 20, 2006.

This web page is for the Spring 2006 offering of Com S 641 at Iowa State University. The details of this course are subject to change as experience dictates. You will be informed of any changes. Thanks to Curtis Clifton for help with these web pages. Please direct any comments or questions to Gary T. Leavens.