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