日期：
来源：数据派THU收集编辑：数据派THU
来源：专知 本文为书籍介绍，建议阅读5分钟 这本全面和高度可读的教科书教学生如何使用增量方法和验证感知的编程语言Dafny来形式化地推理计算机程序。
《程序证明》一书向大家展示了程序编写规范的意义，以及如何编写连接规范和程序的证明。作者以清晰和幽默的文字，概述了程序推理的基本理论，逐步建立起复杂的概念和应用，直到你对使用对象、数据结构和非微观递归等概念有全面的认知。
以易于阅读和学生友好的风格撰写逐步构建复杂的概念 全面涵盖如何编写证明以及如何指定和验证函数式程序和命令式程序 使用来自真实编程语言的真实程序文本，而不是伪代码 特色引人入胜的插图和动手学习练习
https://mitpress.mit.edu/9780262546232/program-proofs/