Tobias Nipkow and Gerwin Klein: Concrete Semantics with Isabelle/HOL
Springer Verlag, 2014, ISBN 978-3-319-10542-0, http://www.concrete-semantics.org/
The book Concrete Semantics with Isabelle/HOL by Tobias Nipkow and Gerwin Klein introduces students to higher-order logic (HOL) and theorem proving in Isabelle and to semantics of imperative programming languages. The book uses the Isabelle proof assistant and comes with supporting material including slides, exercises, Isabelle theories and a PDF of the book itself, all available at http://concrete-semantics.org
This review is written by Stefan Hallerstede for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community. The review has also appeared in Formal Aspects of Computing (link).
*Concrete Semantics by Tobias Nipkow and Gerwin Klein*
By way of Isabelle/HOL, the book introduces students to higher-order logic (HOL) and theorem proving in Isabelle in Part I and to semantics of imperative programming languages in Part II. The book has been prepared with the help of the Isabelle proof assistant and is available at http://concrete-semantics.org together with supporting material including slides, exercises, Isabelle theories and a PDF of the book itself. Before being exposed to the book, students should have some familiarity with discrete mathematics, set theory, logic and proof. Uses of the reflexive transitive closure (Section 4.5.2) or Cantor’s theorem (Section 5.1), for instance, will otherwise require much attention by the students beyond the main concerns of the book, theorem proving and semantics.
The book is highly suitable for use in class, permitting students to pick up important concepts at an appropriate pace. Part I discusses HOL following the equation “HOL = functional programming + logic”, using a selection of well-chosen examples that develop theories of Boolean and integer expressions. We use the term “theory” here in the sense of the Isabelle proof assistant, referring to a module comprising a collection of declarations, definitions and theorems. Such a theory can be imported by other theories in larger theorem proving projects. The authors pay attention to presenting theorems and proofs in a format that can be easily followed alongside in the Isabelle proof assistant. Informal proofs are discussed and compared to mechanised variants. Later in the book, both kinds of proof are used in order to avoid the impression of bias and acknowledging their relevance. Very early in the book, use is made of highly automated features of the Isabelle proof assistant. In my experience, this makes formal proof and the use of a proof assistant somewhat mysterious for a beginner. Instead of using auto and similar commands, I prefer to start with subst and similar commands rewriting goals to be proved in small and clear steps. This can be done without problems for the material in the early chapters before switching to higher degrees of automation to be used in Part II. Part II has chapters on operational semantics (big and small step), denotational semantics and axiomatic semantics (Hoare logic), as well as chapters on compilers, types and program analysis. The last chapter treats abstract interpretation. The presentation of the different semantics is at a good level for students accompanied by well chosen theorems, examples and proofs to understand the concepts and relate them. The surrounding explanations are well-written, understandable and always useful.
Formal proofs in the Isabelle proof assistant are introduced first discussing apply-scripts followed by a discussion of Isar proofs. Whereas apply-scripts provide a more direct interaction with the proof assistant by manipulating its goal list, Isar proofs provide a more readable interface mimicking the style informal proofs are written. Surprisingly, in Part II only one Isar proof is given (in Figure 7.4). In practice, writing Isar proofs requires some skill and training. It would be nice to have some more Isar proofs in Part II that exercise the main constructs with the student. In some examples it shows that notational proximity to a software tool such as the Isabelle proof assistant is a two-sided sword. Sometimes readability is sacrificed in favour of immediate tool support and corresponding abilities of a beginner. The price paid is not very high and in my opinion the advantages of the chosen approach outweigh the small disadvantage concerning readability by far: the student can “try out” the given examples and experiment with them. The discussion of abstract interpretation may be too much for one chapter and appears rushed as the chapter progresses. It is an interesting topic but the presentation will typically overwhelm a student, in particular, as some material is left out for reasons of brevity. To be used for studying the topic it could focus on one form of program analysis (from Chapter 10) and treat the corresponding kind of abstract interpretation. This will be sufficient to understand the general principle.
All in all, the book is highly recommended for learning and teaching theorem proving and semantics, picking up a lot of useful knowledge on higher-order logic along the way. The book is well-structured and written to support learning about the two main themes. It may also help to make formal methods more approachable to a larger number of students by offering the possibility to follow the book with a software tool, inviting the student to experiment and succeed in (automatically assisted) formal proof.