\documentstyle{article}
\nofiles
\input{use-full-page}

\begin{document}

\title{Semantic Models for Programming Languages \\
Course Specification}
\author{Gary T. Leavens \\
Department of Computer Science, Iowa State University \\
Ames, IA, 50011-1040 USA \\
leavens@cs.iastate.edu
}
\maketitle

\begin{abstract}
Computer Science 641
studies the semantics of programming languages.
The emphasis in 1994 will be on axiomatic semantics.

This document specifies the course's general and specific objectives.
\end{abstract}

\section{Introduction}

The study of programming language semantics is primarily concerned with the
following questions:
\begin{itemize}
\item
What are the real differences between various programming languages?
How can various languages be compared?

\item
What are good ways to describe features of various programming languages?

\item
How can we use semantic descriptions to design better programming languages?

\item
How can we use semantic description techniques to design better compilers
and interpreters?
\end{itemize}
Com S 641 addresses all these questions to some extent.
Each year the focus is on slightly different areas,
and in Fall 1994 we will focus on the second and third questions.

\subsection{Course Description}

The catalog description of the course is as follows:
\begin{quotation}
Interpretative, denotational, and logically based models of semantics;
application of semantics to program correctness,
language specification, and translation.
(3 credits)
\end{quotation}

Interpretative models are sometimes called ``operational''
and are exemplified by ``structural operational semantics''
(which use rewrite rules) or Landin's SECD machine (an interpreter).
Denotational models are exemplified by the Scott-Strachey approach
which uses functions over various domains as the meanings of programs;
but in certain contexts algebraic structures are also used as denotations.
Logically based models include axiomatic semantics
(e.g., a Hoare logic for partial correctness)
and inference systems used in the study of ``logic-oriented'' languages
(such as Prolog) or type theory.

In 1990 the offering of 641 emphasized denotational semantics and type theory;
we used notes from Carl Gunter (which later became his book
{\em Semantics of Programming Languages\/})
and various papers on type theory.
In 1992 the offering of 641 emphasized operational semantics;
we used the book {\em Essentials of Programming Languages\/}
and also studied a bit about type inference using $\lambda$-Prolog.
In 1994, the emphasis will be on axiomatic semantics (Hoare logics),
using Wim Hesselink's monograph
{\em Programs, Recursion, and Unbounded Choice\/}
and various other texts and papers.

\section{Prerequisites}

The formal prerequisites are successful completion of Com S 531
(theoretical foundations) and Com S 541 (Programming Languages 1).
The skills taught in Com S 531 relevant to Com S 641 include the ability to:
\begin{itemize}
\item
read and write grammars,
parse expressions and evaluate syntax trees,

\item
design and interpret automata, such as finite state machines
and Turing machines,

\item
prove that certain problems are undecidable.
\end{itemize}
These skills will certainly not be the focus of Com S 641,
but they will be useful as building blocks for more specific tasks.

The skills taught in Com S 541 relevant to Com S 641 include the ability to:
\begin{itemize}
\item
Solve problems using the functional, object-oriented,
and declarative paradigms.

\item
Understand the major features of modern programming languages and
their semantics.

\item
Design programming languages or similar systems
and justify your design decisions.
\end{itemize}
The background in semantics you may have from Com S 541 will be sufficient.

Please speak with me if you have any doubts about how your
background matches these prerequisites.
Also speak to me if you are a mathematics graduate student interested
in the course, but do not have all of these prerequisites.

\section{Essential Objectives}

% Performance
In general terms the essential objectives are for you to be able to:
\begin{itemize}
\item
read and write predicate transformer semantics for programming languages,

\item
design a predicate transformer semantics for some subset of a ``real''
programming language,
and argue why the omitted features of that language are unsafe
or difficult to specify,

\item
design, and formally specify using predicate transformer semantics,
part of an ideal programming or specification
language that has features to make
verification easier,

\item
explain the connections of predicate transformer semantics
with: program verification, other semantic formalisms,
and formal specifications,

\item
show how to prove a predicate transformer semantics correct with respect
to a denotational semantics,

\item
do calculational proof of program correctness,
and describe their advantages and limitations,

\item
state the goals and problems of programming language semantics,
what solutions are known and what the various research directions are,
especially in the area of predicate transformer semantics.
\end{itemize}

% Justification

Some familiarity with formal semantic description techniques is helpful
so that you can communicate the results of your work on programming
language design, specification language design, or formal methods to others,
and so that you can read what others have done.
Formal semantic description techniques
are valuable as a tool for specification and programming language designers,
since they help prevent ambiguity.
They can also be of use in software engineering,
where they can be used to reason about properties of a design.
Formal semantic description techniques can also aid in
judging programming or specification language designs,
by revealing hidden interactions between features,
and by giving you a sense of how simple or complex the design is.

Although in my work on the semantics of subtyping I have mostly
used denotational techniques,
I have been impressed with the ability of
authors who use axiomatic semantics to more quickly and succinctly
present semantics of programming languages.
I believe this is because they seem to work at a higher level of abstraction.
Furthermore, the work of such authors seems closer to the practice
of programming, because it is presented within a semantic framework
that is closely tied to reasoning about programs.
Finally, for those of us involved in
the design and semantics of formal specification languages,
work on axiomatic semantics has an obvious application
both as a guide to what features are desirable in a specification
language, and as a way of formally describing the meaning of
such a specification language.

Predicate transformer semantics is a way to use verification
technology to define programming languages.
Each statement in a language is characterized by the way it
transforms preconditions to postconditions.
Dijkstra and his followers have even advocated the direct use
of predicate transformers, such as the weakest precondition transformer
(wp), in program development;
the argument is that such predicate transformers aid calculational proofs.

The application of predicate transformer semantics to real programming
languages will help you see what the capabilities and limitations of
the techniques are, as well as making sure they are well understood.
Limitations of current techniques point out both places to be careful
in language design, and also areas where more research would be fruitful.
Turning this idea on its head, one can design programming languages
that are well adapted to current verification methods.
(Such considerations have motivated the languages Alphard and Euclid.)

Making connections with other kinds of semantics is necessary both
for a thorough evaluation of the utility of predicate transformer techniques
and to appraise which semantic techniques are best for which tasks.
One often needs complimentary descriptions of a programming language
or specification language, both to increase confidence in the correctness
of the semantics and because different kinds of techniques aid
different studies.
For example, operational semantics seem well-suited for studying properties
of implementations;
denotational semantics seem to match the way language designers think
about and describe programming languages.
Because denotational semantics is a good intermediate abstraction
between
predicate transformer semantics and operational semantics,
it is important to see how to prove a predicate transformer semantics
correct with respect to a denotational semantics.

The style of calculational proofs of program correctness
has been advocated by Dijkstra and his followers
as a way to help ensure that no mistakes are made in program proofs.
I also find the discipline of developing proofs without
``pulling any rabbits out of the hat'' admirable
as a way of teaching, learning, and seeking precision.

Knowing the goals and problems of programming language semantics
gives you perspective on the rest of the work.
It also shows possibilities for your own research and what kinds
of ways that programming may be changing in the future.

\end{document}