彭 成，王盼卿

（军械工程学院 河北 石家庄 050003）

自从20世纪60年代中期由于软件规模越来越庞大，结构也越来越复杂，环境的复杂性，应用领域的复杂性，交流的复杂性，爆发了软件危机．软件开发费用和进度失控，软件的可靠性差，生产出来的软件难以维护，用户对＂已完成＂的系统不满意现象经常发生，如何开发软件，以满足不断增长、日趋复杂的需求；如何维护数量不断膨胀的软件产品等一系列问题始终困扰着软件开发人员，为了解决软件危机，软件开发人员提出了两种解决问题的方法，一种就是众所周知的软件工程方法，即把工程的思想引入软件开发，另外一种方法就是形式化方法．形式化方法用于软件开发可以保证软件的正确性。形式化方法基于严格的数学，在软件开发过程中使用数学具有如下优点：数学是准确的建模媒体，能够对现象、对象、动作等进行简介、准确的描述；数学支持抽象，它使得规格的本质可以被展示出来，并可以以一种有组织的方式来表示系统规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格中的矛盾和不完整性，以及用来展示设计和规格之间的一致性情况[1]。

1 形式化方法的发展

形式化方法（Formal Method）的基本含义是借助数学的方法来研究计算机科学中的有关问题.《Encyclopedia of Software Engineering》对形式化方法定义为:“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻划、开发和验证系统”[2]。……