Program verification has an important role to play in the production of critical software. This book is perhaps better described by its subtitle than by its title. The first half carefully introduces logic without reference to software, while the second half develops verification techniques. It is meant as an undergraduate textbook in computer science and is suitable for well-motivated students willing and able to assimilate the chapters devoted to logic. The authors provide the necessary tools to learn. Worked examples illustrate the concepts, and each chapter has a number of exercises to give students practice. Each chapter ends with a very helpful “To Learn More” section, which places the material in context and gives references for further study.

The authors focus on the logical approach--Hoare logic--to the verification of programs. Chapter 1 is a general introduction to a formal approach in software engineering. In chapter 2, the authors give an overview of formal methods, which will be somewhat vague for students new to the material. Chapter 3 carefully covers propositional logic, contrasting validity checking by semantic methods with validity checking using deductive methods. The next chapter presents first-order logic, concluding with a section on first-order theories applying first-order logic to a domain of discourse, for example, one capturing the properties of data structures present in a programming language.

The remainder of the book applies logic to program verification. Chapter 5 uses Hoare logic to verify programs in a simple language with while loops. It introduces preconditions, postconditions, and loop invariants. Chapter 6 shows how to mechanize Hoare logic using the weakest precondition strategy, and discusses how proof tools are needed to establish the validity of the verification conditions. The next chapter deals with errors during the execution of programs. Chapter 8, “Procedure and Contracts,” covers the interprocedural level of program verification.

The last two (brief) chapters apply the verification techniques to C programs. Chapter 9 introduces the ANSI/ISO C specification language (ACSL). Chapter 10 uses the verification tool Frama-C for ACSL-annotated C programs. The seven C programs in these chapters are available for download. It might have been a nice addition to expand the last chapters with more examples of tool use, even though these tools are in development and subject to change.

Overall, this book will benefit its intended readers and will give them a good foundation in program verification that can be used in applications--provided they go further with the use of the tools briefly introduced.