DD2454 Semantics for Programming
Languages
- 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]
- 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
- Inductive definitions and proofs by structural induction
- Natural semantics (aka Big-step operational semantics)
- Equivalence between statements
- Assignment 1: Exercises
1.13, 2.3, 2.7
Class 3 [Chapter 2.2, 2.3] []
- Peer assessment of Assignment 1
- Determinism of While
w.r.t. natural semantics
- The semantic function Sns
- Structural operational semantics (aka Small-step operational
semantics)
- Example: execute while true do skip
under the SOS, from an arbitrary state s
Class 4 [Chapter 3] [Exercise 2.16]
- Configuration graphs and state space exploration
- Extending While
with additional language features:
- abortion
- non-determinism
- parallelism/concurrency/threads
- subroutines/procedures
- Description of Assignment 2
(see main page)
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
- Correctness as semantic equality w.r.t. specification semantics
Class 6 [] [Exercises 4.13, 4.14, 4.19]
- Peer assessment of Assignment 2
- Concluding remarks on operational semantics
- Description of Assignment 3
(see main page)
Part II:
Denotational Semantics and Program Analysis
Class 7 [Chapter 5.1] []
- Introduction to Denotational Semantics
- The meaning of while loops
Class 8 [Chapter 5.2] [Exercises 5.18, 5.21, 5.33, 5.40]
- Peer assessment of Assignment 3
- 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
- Consistency with the operational semantics of While
- Language properties expressed through denotational semantics:
- determinism
- termination
- equivalence of statements
- Description of Assignment 4
(see main page)
Class 10 [Chapter 7.1] []
- Peer assessment of Assignment 4
- Introduction to Program Analysis
- Detection-of-signs analysis: definition
Class 11 [Chapter 7.4] [Exercises 7.28, 7.29]
- Detection-of-signs analysis: examples
- Application to program transformation
- Description of Assignment 5
(see main page)
Part III:
Axiomatic Semantics and Program Verification
Class 12 [Chapter 9.2]
- Peer assessment of Assignment 5
- Introduction to Axiomatic Semantics [rules]
Class 13
- Finding loop invariants
- Rationale for Program Verification
- Proof tableaux: proofs as annotated programs [example-tree]
[example-tableau]
- Description of Assignment 6
(see main page)
Class 14
- Peer assessment of Assignment 6
- Automating verification
- Soundness and completeness of axiomatic semantics
Class 15
- Course Summary
- Exam Preparation
- Course Evaluation