The “for computer science” part of this excellent book’s title initially gave me pause, as it connoted for me a possible compromise of the “logic” part. As a matter of fact, the very opposite is the case here. The book’s predicate logic, equational reasoning, and natural deduction [1,2,3] are complete and rigorous, and are further enforced by the mechanized ACL2 and Proof Pad assistants that are available on the web to readers. ACL2 is a Lisp dialect; it was one of the 17 mechanized theorem provers that, under the auspices of the second author (Gamboa), successfully accepted the challenge of proving the irrationality of the square root of two [2]. Thus, “essential” in the title justly denotes “focus[ed] directly on central themes in computer science,” in the present book’s words.

Fifteen chapters span four main parts: “Logic and Equations,” “Computer Arithmetic,” “Algorithms,” and “Computation in Practice.” The presentation combines propositional/predicate logic, circuit diagrams, and ACL2 text so as to confer the “benefit [of formal methods on] practicing hardware and software engineers.” The book employs an equation-based model of computation, which is tacitly a subset of the lambda calculus (of functional, that is, non-state-space-based programming). “Both hardware and software are ... logic in action.”

The axioms are Boolean algebra equations, such as (*x* or *y*) = (*y* or *x*), and the rules of inference are those of natural deduction. Thus, the classic truth-preserving flow: axioms, rules of inference, theorems. The axiomatic equations of Boolean algebra are enumerated with utmost clarity and completeness in Figure 2.11 and explicitly include extremely useful axioms for “grammatical” parenthesization, namely ((*x*)) = (*x*) [redundant grouping] and (*v*) = *v* [atomic release]. Regarding parentheses in general, I found the following remark very useful: “the added value of omitting parentheses fails to compensate for the extra complexity” that the rules of grammar would then have. The bases for mechanization “make it possible for computers to check that our reasoning follows all the rules, without exception.” This latter is, of course, the point of formal methods. Theorems come from axioms “and from no other source.” Excellent pedagogy.

The (syntactic) turnstile, |-, is introduced in natural deduction rules of inference, which later are very clearly enumerated in Figure 2.15. A defining summary of the book’s philosophy follows:

Many presentations of classical logic begin with deductive reasoning, but we started with Boolean algebra because we will be using logic to reason about digital circuits and software specified in the form of equations .... [...] Accurate modeling of other domains by propositions in logic can be problematic.

These normative comments are very useful, as they obviate potential astray-leading ruminations about those “other domains.”

Chapter 4 elaborates on mathematical induction over natural numbers as a rule of inference. Such things as structural induction (my example) “can be contorted into proofs by mathematical induction.” All software operators (functions) have inductive definitions and can therefore be verified “to a logical certainty,” given the book’s axioms and rules of inference. Chapter 5, “Mechanized Logic,” explains ACL2/Proof Pad’s matching of formula-elements against templates in axioms, which “computers can carry out flawlessly.” Specifications comprise inductive equations that are processed by formalized, mechanized logic. The ACL2/Proof Pad environment accommodates human help with proofs, which is subject to failure and repeated attempts.

The book is not silent on what I call computing’s “stratosphere”; it covers, to some extent, things like the halting problem, the Church-Turing conjecture, and the work of Gödel. It is, however, a considerable strength that its emphasis and powerful rigor are directed toward hardware and software correctness, which is increasingly shown to be a critical need [4].

Part 2, on computer arithmetic, continues in a rigorous manner to elaborate on the software and hardware of computer arithmetic and includes design and proof of an adder of word-width *w*. The proof of theorem {adder-ok} is by mathematical induction. Other topics include two’s complement arithmetic, big-number arithmetic, and the shift-and-add multiplier. Part 3, on algorithms, employs ACL2’s mechanized logic to design and prove a multiplexer (mux) and demultiplexer (dmx), formally characterized, respectively, by axioms mux and axioms dmx. The dmx is used in the merge-sort in the subsequent chapter on sorting.

The next chapter, on search trees, is very hefty and deals with the Adelson-Velskii and Landin (AVL) tree that is so prominent in today’s processing of big data. The subsequent chapter on hashing is a gem and prepares readers for the book’s coverage of how such giants as Google, Amazon, and Facebook deal with huge distributed databases.

Part 4’s treatment of today’s massively parallel and massively distributed processing via MapReduce and Hadoop connects these contemporary super-sized technologies with the rigorous theory and algorithms of the book’s earlier chapters--a great feat indeed. I did not expect to be interested in or enjoy the final chapter, “Generating Art with Computers,” given some past sampling of computer music. I’m very happy to have been wrong; the authors have in fact left me “with an appreciation that simple principles can indeed lead to complex behavior,” such as that engendered by artistic creativity.

This is a work whose demands are very much worth accommodating, as it imparts both the spirit and letter of serviceable formal methods, a critical methodology if there ever was one. I recommend it highly.

More reviews about this item: Amazon