## Introduction to axiomatic semantics

I have released for general usage the chapter on axiomatic semantics of my book Introduction to the Theory of Programming Languages. It’s old but I think it is still a good introduction to the topic. It explains:

- The notion of theory (with a nice — I think — example borrowed from an article by Luca Cardelli: axiomatizing types in lambda calculus).
- How to axiomatize a programming language.
- The notion of assertion.
- Hoare-style pre-post semantics, dealing with arrays, loop invariants etc.
- Dijkstra’s calculus of weakest preconditions.
- Non-determinism.
- Dealing with routines and recursion.
- Assertion-guided program construction (in other words, correctness by construction), design heuristics (from material in an early paper at IFIP).
- 26 exercises.

The text can be found at

https://se.inf.ethz.ch/~meyer/publications/theory/09-axiom.pdf

It remains copyrighted but can be used freely. It was available before since I used it for courses on software verification but the link from my publication page was broken. Also, the figures were missing; I added them back.

I thought I only had the original (troff) files, which I have no easy way to process today, but just found PDFs for all the chapters, likely produced a few years ago when I was still able to put together a working troff setup. They are missing the figures, which I have to scan from a printed copy and reinsert. I just did it for the chapter on mathematical notations, chapter 2, which you can find at https://se.inf.ethz.ch/~meyer/publications/theory/02-math.pdf. If there is interest I will release all chapters (with corrections of errata reported by various readers over the years).

The chapters of the book are:

- (Preface)

- Basic concepts
- Mathematical background (available through the link above).
- Syntax (introduces formal techniques for describing syntax, included a simplified BNF).
- Semantics: the main approaches (overview of the techniques described in detail in the following chapters).
- Lambda calculus.
- Denotational semantics: fundamentals.
- Denotational semantics: language features (covers denotational-style specifications of records, arrays, input/output etc.).
- The mathematics of recursion (talks in particular about iterative methods and fixpoints, and the bottom-up interpretation of recursion, based on work by Gérard Berry).
- Axiomatic semantics (available through the link above).
- Complementary semantic definitions (establishing a clear relationship between different specifications, particular axiomatic and denotational).

- Bibliography

Numerous exercises are included. The formal models use throughout a small example language called Graal (for “Great Relief After Ada Lessons”). The emphasis is on understanding programming and programming languages through simple mathematical models.