Course Outline
Below, you find an outline of the course with required reading and recommended exercises, both based on the course book.
Class 1 [Chapter 1.1] [slides]
- Introduction to Semantics for Programming Languages
- Course goals and syllabus
- Course organization and administration
Part I: Operational Semantics and Language Implementation
Class 2 [Chapter 1.2-1.4, 2.1] [Exercises 1.13, 2.3, 2.7]
- Syntax of the simple programming language While
- Semantics of arithmetic and Boolean expressions [Prolog]
- Definitions and proofs by structural induction
- Natural semantics (aka Big-step operational semantics) [Prolog]
- Description of Assignment 1 (see Assignments)
Class 3 [Chapter 2.2, 2.3] []
- Program termination
- Equivalence between statements [rules]
- Determinism of While
- The semantic function Sns
- Structural operational semantics (aka Small-step operational semantics)
- Configuration graphs and state space exploration [example]
Class 4 [Chapter 3] [Exercise 2.16]
- Peer assessment of Assignment 1
- The semantic function Ssos
- Equivalence of natural and structural operational semantics
- Extending While with additional language features:
- abortion
- non-determinism
- parallelism/concurrency/threads
- procedures
- Description of Assignment 2 (see Assignments)
Class 5 [Chapter 4] []
- Correct implementation of programming languages: approach
- An abstract machine: language and semantics
- A translation of While statements into abstract machine code
Class 6 [] [Exercises 4.13, 4.14, 4.19]
- Correctness as semantic equality w.r.t. specification semantics
- Description of Assignment 3 (see Assignments)
- Description of Lab Assignment 1 (see Labs)
Part II: Denotational Semantics and Program Analysis
Class 7 [Chapter 5.1] []
- Peer assessment of Assignment 2
- Peer assessment of Assignment 3
- Concluding remarks on operational semantics
- Introduction to Denotational Semantics
- The meaning of while loops
Class 8 [Chapter 5.2] [Exercises 5.18, 5.21, 5.33, 5.40]
- Fixed-point theory
Class 9 [Chapter 5.3, 5.4] [Exercises 5.49, 5.50, 5.51, 5.53]
- Summary of conditions for the Fixed Point Theorem
- Back to the denotational semantics of while loops
- Example: the denotation semantics of while ¬(x=0) do x:=x-2 [example]
- Consistency with the operational semantics of While
- Language properties expressed through denotational semantics:
- determinism
- termination
- equivalence of statements
- Description of Assignment 4 (see Assignments)
Class 10 [Chapter 7.1] []
- Introduction to Program Analysis
- Detection-of-signs analysis: Arithmetic and Boolean expressions
Class 11 [Chapter 7.4] [Exercises 7.28, 7.29] [notes]
- Detection-of-signs analysis: statements
- Detection-of-signs analysis: examples
- Application to program transformation
- Description of Assignment 5 (see Assignments)
Part III: Axiomatic Semantics and Program Verification
Class 12 [Chapter 9.2]
- Description of Lab Assignment 2 (see Labs)
- Symbolic execution [notes]
- Introduction to Axiomatic Semantics [rules]
Class 13
- Peer assessment of Assignment 4
- Peer assessment of Assignment 5
- Soundness and completeness of axiomatic semantics
- Proof tableaux: proofs as annotated programs [example-tree] [example-tableau]
- Loop invariants
- Description of Assignment 6 (see Assignments)
Class 14 [Chapter 9.3]
- Peer assessment of Assignment 6
- Automated program verification I
- symbolic execution based verification [notes]