Formal Semantics of Programming Languages

Wolfgang Schreiner
326.514, SS 1999, Start: 11.3.1999
Thu 16:30-18:00, T1010

While the syntax of a programming language is always formally specified, the equally important aspect of definining its meaning is often left to natural language which is ambiguous and leaves questions open. In order to understand the inherent properties of a language (e.g. for constructing a compiler), we should have a deeper understanding. The goal of formal semantics is to reveal the essence of a language beneath its syntactic surface.

This course presents some major methods for defining the meaning of languages and programs and discusses their relationship:

Operational Semantics

A programming language is defined by reduction rules that describe how the initial state of a program is transformed step by step into the terminal state. This view is most useful for understanding the dynamical behavior of a language, e.g., for constructing an interpreter.

Denotational Semantics

A programming language is defined by a valuation function that maps a program into a mathematical object which is considered as its meaning. This view is most useful for understanding the internal logic of a language, e.g., for reasoning about its properties.

Axiomatic Semantics

A programming language is defined by correctness assertions that describe how to draw conclusions about the input/output interface of a program. This view is most useful for understanding the external effects of a language, e.g., for verifying a program.

Students are expected to elaborate small exercises and to present them in class. This includes the development of executable semantics specifications in the CafeOBJ system.

Contents

Denotational Semantics I

(Based on Schmidt)

• Introduction (PostScript Slides)
• Syntax (PostScript Slides)
• Set, Functions, Domains (PostScript Slides)
• Semantic Algebras (PostScript Slides)
• Basic Structure of Denotational Definitions (PostScript Slides)
• Imperative Languages I (PostScript Slides)

Operational Semantics

(Hardcopies of Winskel)

• Operational semantics of IMP
• A proof of the equivalence of language constructs.
• Denotational semantics of IMP.
• Equivalence of the semantices.

Denotational Semantics II

(Based on Schmidt)

• Domain Theory I (PostScript Slides)
• Domain Theory II (Copies of Schmidt)
• Imperative Languages II (PostScript Slides)

Languages with Contexts

(Based on Schmidt)

• A Block-Structured Language (PostScript Slides)
• An Applicative Language (PostScript Slides)
• Compound Data Structures (PostScript Slides)

Axiomatic Semantics

An assertion langauge, semantics of assertions, verification rules, soundness.

Language Design Principles

Languages with types, abstraction, parameterization, correspondence, qualification.

Miscellaneous Topics

Continuations, exceptions, backtracking, coroutines, unrestricted branching.

Exercise

Imperative Interpreter (PostScript)

Design a small imperative programming language, develop its denotational semantics, and implement an interpreter for this language.

A Java Solution (zip file)

Author: Jürgen Hartl.

Literature

Glynn Winskel

  The Formal Semantics of Programming Languages -- An Introduction, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.

David A. Schmidt

  Denotational Semantics -- A Methodology for Language Development, Allyn and Bacon, Boston, MA, 1986.

David A. Schmidt

The Structure of Typed Programming Languages, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.