《程序证明》一书向大家展示了程序编写规范的意义,以及如何编写连接规范和程序的证明。作者以清晰和幽默的文字,概述了程序推理的基本理论,逐步建立起复杂的概念和应用,直到你对使用对象、数据结构和非微观递归等概念有全面的认知。这本全面和高度可读的教科书教学生如何使用增量方法和验证感知的编程语言Dafny来形式化地推理计算机程序。程序证明向学生展示了为程序编写规范意味着什么,程序满足这些规范意味着什么,以及如何编写将规范和程序联系起来的证明。K. Rustan M. Leino以清晰和幽默的笔法,首先概述了程序推理背后的基本理论。然后,他逐渐建立起复杂的概念和应用程序,直到学生们面对使用对象、数据结构和非平凡递归的真正程序。为了强调程序证明的实用性,所有材料和例子都使用验证感知的程序证明语言Dafny,但不需要事先知道Dafny。