Introduction to the Theory of Programming Languages: full book now freely available

itpl_coverShort 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

 

 

Introduction to axiomatic semantics

itplI 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.

Hilbert spaces

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:

Dresden_Hilbert

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.

OOSC-2 available online (officially)

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.

 

Why stop at pronouns?

My adjectives: timid, arrogant, insufferable.

My adverbs: (just one in fact) inadvertently

My gerunds: painstaking, running away, whining

My verbs: irritate, disappoint

My prepositions: notwithstanding, in spite of, away from

My conjunction: even though

A problem child?

The latest issue of the New York Review of Books contains a book review by George Stauffer about Alban Berg with this bewildering sentence about Berg’s childhood:

He showed few signs of musical talent as a youth aside from informal piano lessons, reading through the scores of songs and operas, and playing four-hand arrangements of orchestral and chamber works with his sister, Smaragda.

Well, well… “Aside from”? If you had a child who could only read through lots of opera scores and play four-hand arrangements of symphonies, would you immediately get to the logical conclusion that he is devoid of musical talent?

(Sorry about poor Alban, he is the shame of our family, let’s just hope Smaragda won’t turn out to be such an abject musical failure.)

One way to become a top scientist…

… is to have a top scientist spot your talent and encourage you, however humble your status may be then.

Wikipedia has a terse entry about Dirk Rembrandtsz (with “sz” at the end), presented as a “seventeenth-century Dutch cartographer, mathematician, surveyor, astronomer, teacher and [religious dignitary]” with “more than thirty scientific publications to his name” and various inventions. Seems just like another early scientific career, but digging a bit deeper reveals that the story goes beyond the ordinary.

The reason I looked up Rembrandtsz is that I ran into the following mention in a seminal book about Descartes, by Geneviève Rodis-Lewis (Calmann-Lévy, 1995). I did not know about Rodis-Lewis herself even though I now realize she was an impressive personality with a remarkable if difficult career (there is an entry about her in French Wikipedia). Here is the relevant extract from her book (pages 255-256), part of the story of Descartes’s years in the Netherlands. The translation is mine, as well as comments in brackets.

During the last years of his life in the Netherlands, Descartes had several opportunities to show [his] interest in people of very modest means. Baillet [Descartes’s first biographer, in the 17-th century] did not give the exact date of the first visit of a “peasant from Holland”, a “shoemaker” by trade, who was studying mathematics in books in vulgar language. [That is to say, not in Latin, presumably in Dutch or French.] When he came for the first time to Egmond [Descartes’s residence] and asked to see Descartes, the servants sent him away. Dirk Rembrandtsz “came back two or three months later”, insisting on being brought in. “His external appearance did nothing to help him get a better reception than before.” Descartes was told, however, of the return of this “annoying beggar” who obviously “wanted to talk philosophy with the purpose of getting some alms”. “Descartes sent him some money, which he refused, saying that he hoped that a third journey would be more productive than the first two.” When Descartes heard about this answer, he gave orders to receive him. “Rembrandtsz came back a few months later” and Descartes was able to appreciate “his skill and merit”. He helped him overcome difficulties and shared his method with him. “He added him to the circle of his friends.” Rembrandtsz “became, through studying with Descartes, one of the premier astronomers of this century”.

I find this story moving. The passionate, stubborn autodidact, determined to reach the highest steps in science in spite of miserable circumstances. The rejection by the servants, from instinctive class-based prejudices. The great scientist’s ability to overcome such prejudice and recognize a kindred, noble spirit and his devotion to the pursuit of knowledge. His generosity, his openness, his availability in spite of the many demands on his time. His encouragement to a young, unknown disciple. The numerous encounters which begin as lessons from a master and evolve towards a relationship of peers. And the later success of the aspiring scientist.

Mr. and Mrs. Bei Uns

It is customary for an article to carry some kind of lesson or moral. This one does not. Or to be more exact it does have a lesson, several perhaps, but they are left to the reader to draw.

It is also customary, for an article that is written as a tribute to deceased people, that the writer would have known them. I never knew the protagonists of my chronicle. But my sister and I — along with a dear cousin, and I hope her children and grandchildren — are among the few people who still know they existed. Hence the need for a tribute lest the last traces of their stay on earth vanish forever.

They were German: Louis Bernheimer, born on 5 December 1875 in Issenhausen in Alsace, then part of Germany, and his wife Paola, born in Bayreuth on 12 February 1879, yes, that same Bayreuth where Wagner had premièred his quintessential German opera, Das Rheingold, three years before. They were German and seemingly, as we shall see, very German.

I know little about them, nothing else in fact than reported in this little note. One thing I do know is the nickname by which people in Paris called them behind their backs: “Mr. and Mrs. Bei Uns”. I know it because my father mentioned it to me. Just once, a long time ago, but I remember.

We need a bit of context. Herr und Frau Bernheimer flew Nazi Germany in the thirties with their son Fred, a young professional photographer, and settled to a safe place, or a place they thought was safe: Paris. There Fred met my father’s sister Éliane and married her; they had two children, my cousins. Now we are talking about the only people in this story whom I did know. Éliane was a strong personality, a dedicated feminist and activist. When her husband was hit with cancer and she abruptly found herself a widow with two young children and no resources, she took over his photography studio, learned the trade — about which she had known nothing — and made the business prosper. After the war, Studio Bernheim (the name shortened so that it would sound less German) became one of the fashionable addresses in Paris, thanks to both Éliane and her son Marc who trained himself to become its chief photographer while still a teenager.

Bei uns in German means the same as “chez nous” in French and translates as “at our home”, although that is not a good translation because English lacks a preposition that would accurately reflect the French “chez” or (in that sense) the German “bei”, which mean something like “in the home of”.  “Home” in a very intense and cozy sense, not just the physical house, but encompassing culture, country, community. Russians similarly say “U Nas”, literally “at ours” and, when talking about people, “Nashi”, literally “ours”, our people that is. In a Chekhov novella entitled  A boring story (full text available online here), when the antisemitic narrator wants to mention that at the theater last night the person seated in front of him was a Jew, he says that he was sitting behind an “iz nasikh”, a deformation with a fake Jewish accent of “iz nashikh”, one from our own, to suggest — ironically in light of the rest of my own boring story — a member of a tightly knit community.

It seems that the Bernheimers (to come back to them) were seen by their new extended family as stuffy Germans fitting the stereotypes. Not just stuffy: critical. Apparently, they went around commenting that whatever was being done in their new French surroundings was not being done right, and explaining the way it was done back home, “bei uns”. If so, it was perhaps not the best way to ingratiate themselves with their hosts, and it is not surprising that people in the family started referring to them acerbically, according to my father, as Mr. and Mrs. Bei Uns.

As noted, I never knew the Bernheimers, although in a different turn of the story I would — I should — have known them as a child. Therefore I cannot guess whether I would have yielded to family opinions and found them insufferable, or liked them as delightful, exotic older relatives having gone through hard times and now doting on their children, grandchildren, nephews and nieces. Maybe both. I feel a certain remote sympathy for them in any case, having probably been resented, like anyone who has lived in countries where people insist on the “korrekt” way of doing things and comes back to more lackadaisical cultures, as a bit of a Mr. Bei Uns myself.

The irony is that in the eyes of many people, including many who would never consider themselves antisemites, Jews still have the reputation of harboring a feeling of  solidarity with their own kin that transcends borders and trumps national allegiance. Here we have the reverse. Highly assimilated families on both sides, French Jews and German Jews, getting into a cultural conflict because some were French and some were German. Ever since the revolution emancipated French Jews, they have been passionately French. German Jews were just as passionately German (in the style of Heinrich Heine’s I think of Germany in the night, the poem entitled Nachtgedanken, written in exile in Paris, see its text here).  French Jews do not ask themselves how French their are, since their Frenchness is as obvious to them as the air they breathe; it’s others who want them to prove it again and again — something that no one ever seems to require of people from certain regions of France such as Brittany whose inhabitants have a loudly proclaimed attachment to their terroir of origin. Unbelievably, the question still resurfaces regularly; it is even a theme in the current presidential campaign.

Why did I never get to decide by myself who Mr. and Mrs. Bei Uns really were: chauvinistic scolds, or a charming old-world couple? If they thought of themselves as German, as part of “uns”, the “uns” ruling Germany had a different understanding. When Germany invaded France in 1940, the Bernheimers flew, like many others, to the South of France, which until 1942 remained a supposedly “free” zone. Then the Germans invaded the “free” zone too. In August of 1943 Mr. and Mrs Bei Uns were rounded up near Bayonne. The town is close to the Spanish border; I do not know if they had hoped to cross over, as others managed to do. They were interned in the Mérignac camp, where Bordeaux airport lies today. From Bordeaux they were transferred to the infamous camp at Drancy, near Paris. From there they were put on convoy number 26 to Auschwitz, where they were murdered.

PhD and postdoc positions in verification in Switzerland

The Chair of Software Engineering, my group at the Schaffhausen Institute of Technology in Switzerland (SIT), has open positions for both PhD students and postdocs. We are looking for candidates with a passion for reliable software and a mix of theoretical knowledge and practical experience in software engineering. Candidates should have degrees in computer science or related fields: a doctorate for postdoc positions, a master’s degree for PhD positions. Postdoc candidates should have a substantial publication record. Experience is expected in one or more of the following fields:

  • Software verification (axiomatic, model-checking, abstract interpretation etc.).
  • Advanced techniques of software testing.
  • Formal methods, semantics of programming languages.
  • Concurrent programming.
  • Design by Contract, Eiffel, techniques of correctness-by-construction.

Some of the work involves the AutoProof framework, under development at SIT (earlier at ETH), although other topics are also available, particularly in static analysis.

Compensation is attractive. Candidates must have the credentials to work in Switzerland (typically, citizenship or residence in Switzerland or the EU). Although we work in part remotely like everyone else these days, the positions are residential.

Interested candidates should send a CV and relevant documents or links (and any questions) to bm@sit.org.

Panel on methodology and agility, this Monday (20 September)

Today (well, tomorrow as of writing, but when you see this it will probably be today for you) I am participating in a panel discussion with Ivar Jacobson, Robert Martin and Carlos Zapata on “The Future of Methods”, hosted by the SEMAT/Essence movement. It takes place at 18:30 CET (i.e. Paris/Zurich etc.), 12:30 EDT, 9:30 in California. It’s free, but requires registration at https://www.meetup.com/essence-for-agility/events/280316615/.

Should be a good discussion!