形式化方法（当时我就只翻译了这一段，因为我认为还是直接读原文更好）

在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。^[1]

Incomputer scienceandsoftware engineering,formal methodsare a particular kind ofmathematically-based techniques for thespecification, development andverificationofsoftwareandhardwaresystems.^[1]

将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，

使用适当的数学分析以提高设计的可靠性和鲁棒性。^[2]

The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.^[2]

但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。^[3]

However, the high cost of using formal methods means that they are usually only used in the development of high-integrity systems,^[3]wheresafetyorsecurityis of utmost importance.

^from：

http://en.wikipedia.org/wiki/Formal_methods

http://en.wikipedia.org/wiki/History_of_software_engineering