K. Rustan M. Leino: Program Proofs
MIT Press, 2023, 496 pp, ISBN: 978-0-262546-23-2. https://mitpress.mit.edu/9780262546232/program-proofs/
Summary
The book Program Proofs by Rustan Leino teaches students how to write specifications for functional, imperative, and object-oriented program code and how to prove them correct. The book uses the language and proof tool Dafny. It comes with online code examples and, as teacher’s material, answers to the exercises.
This review is written by Kees Huizing 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.
Program Proofs
by
K. Rustan M. Leino.
Review
Teaching program verification can highly benefit from a tool that checks the specifications and, ideally, proves them. The Dafny verification system is such a tool. Dafny is open-source and operates directly on the program, which can be annotated. It does not require additional knowledge of and activity in theorem provers. Finally, there is a book that supports this approach, written by the prime developer of Dafny himself.
Dafny is a programming language with the typical imperative and object-oriented features. Additional to this, annotations can be written in the program to specify with pre- and postconditions the intended behavior of the program and to support the correctness proof with assertions, invariants, functions, predicates, and lemmas. Actually, this part could be considered a functional language on its own, with many of the typical features of functional programming language. The Dafny tool, integrated in the IDE (typically Visual Studio Code), generates from an annotated program verification conditions, sends these to the prover (the SMT solver Z3) and provides feedback in the program code about its results. When the proofs of all verification conditions succeed, the program is correct, relative to the annotation. This allows for a developing process where writing code is integrated with its verification. The developer deals with this verification on a relatively high level, communicating with the prover on the level of the program, by means of the annotations, and leaving proof details to the automated prover.
The book consists of three parts. The first part explains the basics of specification and proofs. The second part treats formal verification of functional programs. It should be noted that the language contains a decent functional subset, to support the specification of programs, among other things. For those who are only interested in proving imperative programs, they can skip this part and continue halfway the book with the third part. This part deals with classical imperative programs such as binary search and quicksort, but also with object-oriented programs, where objects with identity are modified, exploiting dynamic frames for correctness.
The book contains a lot of in-text exercises, to support the learning of the concepts and skills treated. Each chapter concludes with a summary and a notes section that briefly gives the scientific history of the presented concepts and alternative approaches in the field. Illustrations throughout the book provide what the word says, i.e., some enlightenment.
Program Proofs is an important and original book about program verification. This is a broad topic, however, and to clarify what the focus of the book is, we first tell you what this book is not about.
What this book is not
For those who are looking for a text book for a theoretical course on program verification, this may not be the book. It does not really give a semantics for the programming language and it does not give a proof system either. It does give, though, a decent treat of weakest preconditions and strongest postconditions that are presented as the basis of verification.
Program Proofs also steers clear from the nasty, or, if you like, more advanced parts of tooled verification. Most of the programs are such that they verify without much human effort on the proofs as such. For example, functions on sequences (immutable arrays) are usually defined with additional parameters that specify the segment of the sequence that the function is working on, which keeps the verification simple. An alternative approach, where a segment of the sequence is provided as an argument, where no additional segment parameters are needed, is arguably more elegant, but will be confronted with more proof effort from the human, because simple properties about segments of sequences are not automatically inferred by Dafny. Nevertheless, with this limited amount of human effort, a lot of interesting programs are verified, forming an impressive presentation of the power of the tools.
Related to this, the book does not tell you much about the workings of verification tools and the underlying theorem provers. It treats these as a black box. For more advanced verification efforts, knowledge about the workings of the proof tool, its strengths, and weaknesses may be helpful in finding a verifying annotation.
Another thing this book does not do is giving an extrinsic motivation for formal program verification. It does not provide the obligatory introduction to a course or lecture on program verification where the demise of the Ariane 5 or other software induced catastrophes are brought back to memory. We can probably do without these, but some ideas or a vision on how the presented techniques and tools could be effectively embedded in the industrial processes of software development.
The book explicitly states that it expects from the reader some decent knowledge of (formal) logic. This is indeed the case. The appendix contains a short introduction to logic, but this is not enough to learn logic from, and probably enough to be able to follow the proofs and do the exercises, for instance those in Chapter 2.
What this book is
All this being said, what we do have is a long awaited exposition of state-of-the-art program verification with at-the-code tool support. The book can serve as an introduction to this field for any interested computer scientist. It is also a solid and very well readable text book that can be used in courses for undergraduates, with some training in logic, and graduates to teach the effectiveness of modern program verification as well as the beauty of algorithms and their correctness proofs.