In an ideal world, the “correctness” problem in computer science (CS) would be tackled mainly by teaching the programmer to design the code correctly, from the beginning, for formal verification using appropriate tools. In the real world, however, programmers often confront the difficult problem of starting with legacy code, having to analyze it to understand what it actually implements. This book addresses the real-world situation, and presents a path-oriented program analysis method that can be applied to a reasonably wide range of programs, to gain insight into what the code does and to provide a measure of confidence in its correctness.

The very narrow focus of this book--just one useful technique for decomposing programs along various execution paths, and then recomposing them into an equivalent, but easier to understand, version--is, simultaneously, both its strength and its weakness. Its strength, because it allows a very elaborate treatment of the topic, with meticulously worked-out examples; this will surely help the reader grasp the ideas well and use them on other similar programs. Its weakness, because it does not address the bigger context in which this method fits, including whether it can be combined with other methods to handle other common programming language features, such as complex data types, function calls, and recursion. A chapter on how it compares with other methods, such as program slicing, would also have been very useful.

This book will definitely be a useful resource when teaching certain parts of a course (such as compilers, program analysis, and program verification). As Huang indicates, the value of this path-oriented method will be substantially enhanced if most of the work can be done by an automated tool instead of by hand. Building parts of such a tool would be an interesting term project for students.