小教父（麻省理工出版社）

一个关于计算机程序的书面证明的介绍，以易于理解的问答方式编写，包括逐步的例子和一个简单的证明助手。
小证明者引入归纳证明作为一种确定计算机程序事实的方法。它以平易近人、引人入胜的问答风格写成，带有《小阴谋家》（MIT出版社第四版）特有的幽默感。有时候学习的最好方法就是坐下来做；这本书通过一步一步的例子告诉读者如何写归纳证明。Little Prover只假设了解递归程序和列表（如Little Schemer的前三章所述），只使用了一些新手程序员已经知道的术语。这本书配有一个简单的证明助手，帮助读者通读这本书，并为每个例子提供完整的解决方案。
The Little Prover (The MIT Press)
An introduction to writing proofs about computer programs, written in an accessible question-and-answer style, complete with step-by-step examples and a simple proof assistant.
The Little Prover introduces inductive proofs as a way to determine facts about computer programs. It is written in an approachable, engaging style of question-and-answer, with the characteristic humor of The Little Schemer (fourth edition, MIT Press). Sometimes the best way to learn something is to sit down and do it; the book takes readers through step-by-step examples showing how to write inductive proofs. The Little Prover assumes only knowledge of recursive programs and lists (as presented in the first three chapters of The Little Schemer) and uses only a few terms beyond what novice programmers already know. The book comes with a simple proof assistant to help readers work through the book and complete solutions to every example.

OR