本文共 607 字，大约阅读时间需要 2 分钟。

什么是形式化方法？

在百度百科上，提到形式化方法在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式。 在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。 在软件工程中，形式化方法指的是建立在严格数学基础上的软件开发方法。在关键系统的设计中，一个微小的bug可能会造成重大的错误，人们常常在写出代码后进行各种测试找出系统的bug，而这其实上是不够可靠的，一般来说，工程师会根据个人及测试人员等的建议下，根据直觉或统计信息对代码做更改，而这样是无法穷尽罕见事件的集合的，代码可达的状态会是一个天文数字。所以，为了找到系统中难以发现的bug，对系统做出更精确的设计，同时，由于系统不可避免的复杂性，我们需要一种具有高度表达性，抽象高于代码，有精确语义的方法。形式化方法或许是一种可以开发出完全正确的系统的工具。

原文链接：

https://baike.baidu.com/item/%E5%BD%A2%E5%BC%8F%E5%8C%96%E6%96%B9%E6%B3%95/4298196#3