## 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:

- Meetings
- Course Textbooks
- Accommodations for Disabilities
- Course Description
- Objectives
- Prerequisites
- 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**.

## Course Textbooks

There is one required text for the course.

- Principles of Program Analysis, by Flemming Nielson, Hanne Riis Nielson, and Chris Hankin (Springer-Verlag, 1999). ISBN 3-540-65410-0.

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.

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

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

## 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:

- Explain the goals of program analysis how it can be used in tools for programming and specification languages, as well as its advantages, disadvantages, and limits [A1] [B1] [B3] [C2].
- Judge and improve the quality of various kinds of program analyses, including data flow analysis, constraint based analysis, abstract interpretation, and type and effect systems [A1] [B1] [B3].
- Explain and generalize the mathematical ideas that are used in various program analysis techniques [A1] [A2] [C2]
- Apply program analysis techniques to calculate various properties of small programs [A1] [A2] [B1] [B3].
- Use and explain operational semantic descriptions of programming languages [A1] [A2].
- Prove the soundness of an analysis with respect to the operational semantics of a language. [A1] [A2] [B3].

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.

- Use and explain denotational descriptions of programming languages [A1] [A2].
- Apply program analysis tools, such as TVLA [A2] [A3].
- Use algebraic or calculational techniques to modify, derive, and prove analyses correct [A2].
- Explain why some programming langauge or specification langauge features are harder to analyze than others [C2].
- Explain the research and scientific questions that are open in the area of program analysis [A1] [B3] [C2].

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

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

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.