Bertrand Meyer's technology+ blog

Short version: the full text of my Introduction to the Theory of Programming Languages book (second printing, 1991) is now available. This page has more details including the table of chapters, and a link to the PDF (3.3MB, 448 + xvi pages).

The book is a survey of methods for language description, particularly semantics (operational, translational, denotational, axiomatic, complementary) and also serves as an introduction to formal methods. Obviously it would be written differently today but it may still have its use.

A few days ago I released the Axiomatic Semantics chapter of the book, and the chapter introducing mathematical notations. It looked at the time that I could not easily  release the rest in a clean form, because it is impossible or very hard to use the original text-processing tools (troff and such). I could do it for these two chapters because I had converted them years ago for my software verification classes at ETH.

By perusing old files, however,  I realized that around the same time (early 2000s) I actually been able to produce PDF versions of the other chapters as well, even integrating corrections to errata  reported after publication. (How I managed to do it then I have no idea, but the result looks identical, save the corrections, to the printed version.)

The figures were missing from that reconstructed version (I think they had been produced with Brian Kernighan’s PIC graphical description language , which is even more forgotten today than troff), but I scanned them from a printed copy and reinserted them into the PDFs.

Some elements were missing from my earlier resurrection: front matter, preface, bibliography, index. I was able to reconstruct them from the original troff source using plain MS Word. The downside is that they are not hyperlinked; the index has the page numbers (which may be off by 1 or 2 in some cases because of reformatting) but not hyperlinks to the corresponding occurrences as we would expect for a new book. Also, I was not able to reconstruct the table of contents; there is only a chapter-level table of contents which, however, is hyperlinked (in other words, chapter titles link to the actual chapters). In the meantime I obtained the permission of the original publisher (Prentice Hall, now Pearson Education Inc.).

Here again is the page with the book’s description and the link to the PDF:

bertrandmeyer.com/ITPL

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)

1. Basic concepts
2. Mathematical background (available through the link above).
3. Syntax (introduces formal techniques for describing syntax, included a simplified BNF).
4. Semantics: the main approaches (overview of the techniques described in detail in the following chapters).
5. Lambda calculus.
6. Denotational semantics: fundamentals.
7. Denotational semantics: language features (covers denotational-style specifications of records, arrays, input/output etc.).
8. 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).
9. Axiomatic semantics (available through the link above).
10. 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.

In the heavy context of current news I hope it is permissible to engage in lighter observations. Some time ago I was briefly in Dresden, in the midst of a mayoral election campaign, and I noticed posters for this candidate:

“Dirk Hilbert, Competent For Dresden”. Apparently it worked since he is now mayor, but do you not find the motto a bit on the bland side?

If anyone knows who will be doing his campaign’s PR for the next election, please put me in touch. If my name were Hilbert and I were running for office, I would demand better slogans from my team. Even if I were so power-hungry as to want to appeal to both sides on controversial issues.

Immigration for example:

• Pro-immigrant: Dresden hat Raum für mehr (Dresden has room for more!).
• Anti-immigrant: every spot is  already occupied!

On the environment too, one can, as any good politician, adapt to the audience:

• Animal-rights: Mehr Löcher für mehr Tauben (more holes for more pigeons!).
• Anti-animal-rights, pro-hunting-lobby: “We could kill half the pigeons, no one would notice!”. (Two thirds! Ninety-nine percent!).

Lots of potential on environmental and business issues as well:

• Pro-growth, pro-business: Extra rooms without the extra cost!
• Anti-growth: Dresden braucht kein neues Hotel! (Dresden does not need any new hotel.)

I can also see possibilities in inspirational-style slogans:

• Yes, I Can More Than I Can!
• Make Dresden Great Again! (Without Actually Changing It.)
• Build Back Infinitely Better.

Or a simple one focusing on the candidate himself:

• The natural and rational choice.

The possibilities seem limitless, although I hesitate to say innumerable. As always in politics, the hard part will start when things get real.

My book Object-Oriented Software Construction, 2nd edition (see the Wikipedia page) has become hard to get. There are various copies floating around the Web but they often use bad typography (wrong colors) and are unauthorized.

In response to numerous requests and in anticipation of the third edition I have been able to make it available electronically (with the explicit permission of the original publisher).

You can find the link on another page on this site. (In sharing or linking please use that page, not the URL of the actual PDF which might change.)

I hope having the text freely available proves useful.