形式化方法

在计算机科学中，形式化方法是用于软件和硬件系统的规范、开发和验证的数学上的严格的技术。在软件和硬件设计中使用形式化方法的动机是希望像其他工程学科一样，进行适当的数学分析能够有助于提高设计的可靠性和稳健性。形式化方法采用了各种计算机科学的理论基础，包括逻辑计算、形式语言、自动机理论、控制理论、程序语义学、类型系统和类型理论。

半正式方法是指不被认为是完全"正式"的形式主义和语言。它把完成语义的任务推迟到以后的阶段，然后通过人的解释或通过代码或测试用例生成器等软件进行解释。

形式化方法可以在多个层次上使用。第0级：可以进行正式的规范，然后非正式地开发一个程序。这被称为正规方法的精简版。在许多情况下，这可能是xxx成本效益的选择。1级：形式化开发和形式化验证可以用来以更正式的方式产生一个程序。例如，可以进行属性证明或从规范到程序的细化。这可能最适合于涉及安全或安保的高集成度系统。第二级：可以使用定理证明器来进行完全正式的机器检查证明。尽管工具在不断改进，成本在不断下降，但这可能是非常昂贵的，只有在错误的成本非常高的情况下（例如，在操作系统或微处理器设计的关键部分）才是实际值得的。有关这方面的进一步信息将在下面展开。与编程语言语义学一样，形式化方法的风格可以粗略地分类如下。指称语义学，其中系统的意义在域的数学理论中被表达。这类方法的支持者依靠领域被充分理解的性质来赋予系统以意义；批评者指出，并不是每个系统都可以直观或自然地被看作是一个函数。操作语义学，其中系统的意义被表达为一个(大概)更简单的计算模型的动作序列。

这种方法的支持者指出，他们的模型的简单性是达到表达清晰的手段；批评者则反驳说，语义学的问题只是被拖延了(谁来定义更简单的模型的语义？)。公理语义学，其中系统的意义被表达为前提条件和后置条件，这些条件在系统执行任务之前和之后分别为真。支持者注意到与经典逻辑的联系；批评者注意到这种语义从来没有真正描述过系统做了什么（仅仅是之前和之后的真实情况）。轻量级的形式化方法一些从业者认为形式化方法社区过分强调了规范或设计的完全形式化。他们认为，所涉及的语言的可表达性，以及被建模的系统的复杂性，使得完全形式化成为一项困难和昂贵的任务。作为替代方案，已经提出了各种轻量级的形式化方法，它们强调部分规范和重点应用。这种轻量级的形式化方法的例子包括Alloy对象建模符号，Denney将Z符号的某些方面与用例驱动的开发综合起来，以及CSKVDM工具。

形式化方法可以在开发过程中的不同阶段应用。

形式化方法可以用来描述要开发的系统，无论需要什么级别的细节。这种形式化的描述可以用来指导进一步的开发活动；此外，它还可以用来验证正在开发的系统的需求是否被完整和准确地指定，或者通过用一种具有精确和明确的语法和语义的形式化语言来表达系统需求。