This text should be considered for an introductory course in programming language theory and implementation for advanced undergraduates or beginning graduate students. The author presents a concise overview of methods, issues, and developments in both imperative and functional language verification. His discussion is evenhanded and does not get bogged down in details or theory. The book contains numerous examples and exercises that reinforce material immediately after it has been presented and ends with a good bibliography. Gordon provides an informative historical sketch of the relevance of the lambda calculus to contemporary functional program verification theory, as well as some historical commentary on LISP.
Part 1 presents the axioms and rules of Floyd-Hoare logic, illustrating them on a small Pascal-like programming language, and offers an approach to mechanizing program verification. The semantics of WHILE commands is badly botched near the beginning of the book. Fortunately, the book appears relatively free of errors otherwise.
Part 2, “The Lambda Calculus and Combinators,” begins with an introduction to the syntax and semantics of the lambda calculus, then discusses how the lambda calculus can represent various data objects and recursive functions. The author illustrates functional programming with a small functional programming language and presents an algorithm to compile from this language into lambda expressions. A chapter on combinators, which includes an introduction to reduction machines and algorithms (due to Curry and Turner) for compiling lambda expressions into combinators, concludes this part. In a separate chapter, the author presents the Church-Rosser and normalization theorems, and the theorem on the undecidability of the halting problem, and explains their significance for functional language implementation theory.
Part 3 contains a brief introduction to LISP that includes a discussion of the advantages and disadvantages of dynamic binding. The author then provides code in Franz LISP for a simple theorem prover, a program verifier, and a lambda calculus toolkit (parser, reducer, and translator to combinators). Each section of code is explained. I keyed in and ran the theorem prover (using LISZT VAX version 8.36): the example on page 192 did not, however, evaluate to T as it should have. Instead, the theorem prover wrote out the original implication, substituting X for each occurrence of 1, which gave
:.PD8 :.OC :.HB (((X=(((N − X) * N) DIV 2) and ((X <= N) and (N <=M )))
implies ((X + N)=(((N + X) − X) * (N + X)) DIV 2))).:.OE :.HT