形式化方法是计算机科学理论中历史最悠久、理论性最 强、也最高度发达的学科之一，该学科最早起源于二十世纪 初期纯数学领域中对数理逻辑、可计算性、证明论等基础研 究，并逐渐发展为计算机科学的重要分支之一。

形式化方法主要用数学的理论和工具，对计算机软硬件 系统进行形式建模并进行性质推理研究，以期证明系统的实 现正确性、或提高系统的可靠性和健壮性等。形式化方法和 计算机软硬件很多领域的的研究深入交叉融合，在形式语言 与自动机、软件系统建模与软件可靠性证明、霍尔逻辑与程 序验证、程序合成、符号执行与软件测试等研究领域都有重 要应用。尤其在进入二十一世纪这二十多年来，随着自动定 理证明工具的成熟，且伴随着大数据、云计算、区块链等新 兴技术的发展，形式化方法在一键式证明、云服务安全架构、 智能合约证明等新领域也得到愈加广泛的应用。

本教材和专著对形式化方法理论和典型应用做了全面讨 论和介绍，在本书的准备过程中，我们特别注意把握了以下 三个原则：第一，理论性：本书特别强调了基础理论的重要 性，从实现理论完备性的目标出发，本书对形式化方法涉及 的基础理论都给出了充分的讲解，这些重要理论包括但不限 于形式化方法的基础知识、命题逻辑、布尔可满足性、一阶逻 辑、可满足性模理论、等式与未解释函数、线性算术理论、数 据结构相关理论、理论组合等等。这部分内容将给学生打下 坚实的理论基础。

第二，应用性：本书特别强调了理论的实际应用，对当 前形式化方法重要的应用领域都做了充分介绍，并给出了大 量实例；这些重要的应用领域包括包括符号执行、程序验证、 程序合成、类型理论等等。通过这些应用，学生有机会看到这 些形式化理论，是如何被用于解决重要的实际研究问题。

第三，实践性：本书适当增加了对新技术和前沿研究的 讨论和介绍，并特别增加了形式化方法的最新实践，提供了 对Coq、Z3、KLEE、Dafny、Rosette、Twelf、F* 等最新软件 工具的介绍；我们认为，在一本主要面向高年级本科生和研 究生的教材和专著中，适当增加对学科前沿新技术和实践的 研讨，有助于学生尽快进入相关专题的专门研究。

本书内容共分十三章。我们从讨论必要的基础知识出发 （第一章）；进入对数理逻辑基础的讨论（第二、四章），这部 分内容涵盖了命题逻辑、谓词逻辑，详细讨论了这些形式系 统的语法、语义、及其关键性质。接下来，我们重点讨论可 判定性问题和重要的决策过程，包括可满足性问题（第三章）、 等式和未解释函数理论（第五章）、线性算术理论（第六章）、 数据结构理论（第七章），以及理论组合（第八章）。最后，我 们讨论理论的若干重要应用，包括符号执行（第九章）、程序 验证（第十章）、程序合成（第十一章）、Curry-Horward 同构 （第十二章），和依赖类型（第十三章）等。

笔者特别感谢中国科学技术大学李曦教授在课程教学和 内容组织方面，给笔者提供的无私指导和支持；特别感谢软 件学院王超副院长，在课程建设和课程项目立项上，提供的 大力帮助。

本书是笔者在中国科学技术大学软件学院所讲授的形式 化方法等相关课程讲稿的基础上综合整理而成；笔者特别感 谢樊淇梁和潘志中两位助教，他们全程听课和记录了课程笔 记，并在将笔记整理成书稿的过程中，做出了极大贡献。

本书得到中国科学技术大学研究生教育创新计划支持。

限于作者的知识水平和时间，书中不妥甚或谬误之处在 所难免，恳请读者指正。

华保健
于中国科学技术大学软件学院