浅析形式化描述方法的应用
浅析形式化描述方法的应用
文/冯松军
形式化方法是一种使用严格的数学模型和方法准确、抽象、
规范地描述和验证软件系统的行为和性能的方法，其中主要包括
软件的需求规格、设计和实现等。使用这种描述方法可以帮助开发
者发现软件系统的设计、实现和程序中的问题和缺陷，能够较好
的提高软件系统的正确性和可靠性。本文介绍了形式化方法的基
本内容、分类以及应用等方面，分析了其思想和应用情况，以及
形式化方法在软件工程中的优势和可靠性，并列举了一个简单的实例。
【关键词】软件工程 形式化描述 形式规约语言 Z 语言
1 引言
随着计算机硬件和应用技术的快速发展，软件工程和软件开发技术也发展迅速，那么在
这种情况下，开发出正确的、可靠的、安全的、可扩展的、结构复杂的软件就变得越来越重要，
形式化描述方法的出现成为了解决此问题的一种方法。软件工程和设计模式的规格和功能描
述可以采用非形式化和形式化描述两种方法，非形式化的描述方法主要有自然语言、流程图
等，但是这种方法存在一定的局限性、不准确性和易混淆性。而形式化描述方法则是使用严
格的数学方法进行描述，并且具有严格的语法和语义定义，可以准确、抽象、规范地描述软
件系统的模型、功能和规格，从而提高软件的正确性和可靠性，更好地满足用户的需求。
2 形式化方法的介绍
2.1 形式化方法的含义
形式化方法（Formal Method）的基本含义是借助数学的方法来研究计算机科学中的有
关问题。形式化方法提供了一个框架，在框架中可以用数学的方式开发和验证系统。在软件
开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都可称为形式化的方法。总之，形式化方法是软件开发过程中
规格、设计及实现的系统工程方法，是软件规格和验证的方法。而形式化的软件开发就是用
形式化语言来描述软件的需求和功能，并通过推理验证来保证最终的软件系统实现了这些需
求和功能。形式化方法的规格描述所采用的形式化描述语言是严格的数学语言，其语法和语
义都是无二义的、精确的，目前形式化规格描述语言主要有 Z 语言、VDM 语言等。因为形
式化方法使用具有精确的、一致性的和完整性的数学符号来描述软件系统，因此只要保证软
件规约对实际问题描述的正确性，就能确保软件系统实现的完备性与可靠性。
2.2 形式化方法的内容
软件开发的形式化描述方法有两个重要内容：形式规约 (Formal Specification) 和形式
验证 (Fomal Verification)。形式规约是用具有精确语义的数学语言描述程序的功能，它是
设计和编写程序的依据。其中典型的是基于状态的描述方法，利用一些已知特性的数学抽象
（域、元组、集合、序列、包、映射等）来为软件系统的状态特征和行为特征构造模型。形
式验证与形式规约之间有着密切的联系，形式验证就是验证最终的程序是否满足其规约的要
求，这是形式化方法重要的问题。形式化方法是用数学方法解决计算机科学研究和软件工程
中程序开发问题的工具，集合论、数理逻辑、代数理论、范畴论、抽象构造类型论等数学理
论是形式化方法坚实的理论基础。在形式化描述中，数据抽象和过程抽象
是软件规格过程中的两类重要抽象。数据抽象又称为表示抽象，是利用抽象的数据结构（如
关系、函数等）来进行功能性的描述，而不关心这些抽象数据结构在计算机中是如何表示和
实现的；过程抽象是指忽略任务具体完成的过程，而只精确描述该任务所要完成的功能，即
描述了从输入到输出的映射，该映射的定义域和值域均使用数据抽象来刻画。
2.3 形式化方法的分类
根据表达的方法和性能，形式化方法可以分为五类：
（1）面向模型的方法：也称为基于状态的形式方法，利用一些已知特性的数学抽象，
如集合、序列、映射等为目标软件的状态特征和行为特征构造模型，如 Z 语言。
（2）代数方法：通过分析不同操作间的行为关系给出操作的隐式定义，而不定义状态，
支持描述的结构化，代数方法仅使用一阶逻辑表示，如 OBJ 语言。
（3）基于过程代数方法：给出并发过程的一个显式模型，并通过过程间的约束来表示行为。
（4）基于逻辑的方法：采用逻辑描述系统的特性，包括程序行为的低级规范和系统行为规范，使用与所选逻辑相关
的公理系统证明系统具有预期的性能。如时态逻辑。
（5）基于网络的方法：根据网络中的数据流显式地给出系统的并发模型，包括数据在网中从一个结点流向另一个结点的条件。
如 Petri 网。
3 形式化方法的评论形式化方法在软件开发各阶段的应用能
有效地提高软件质量和开发效率，减少开发成本。形式化描述的优势在于实际问题的抽象和
语法准确、语义清晰、描述准确规范、表达无二义性。形式化方法还可以通过数学工具求解
一些问题的确定解进行有效地检查软件系统中的非功能特性。
4 Z语言与形式化应用实例
4.1 Z语言
Z 语言是由英国 Oxford 大学程序研究组设计的一种基于一阶谓词逻辑和集合论的形式
规格说明语言，它采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说
明。它支持形式化方法中的两种类型的抽象，并分别称之为表示抽象和操作抽象。在表示抽
象中，数据从数据结构的表示细节抽象出来，使用关系、函数、集合、序列、包等抽象的数
据类型，这些类型构成 Z 语言的类型系统；而操作抽象则描述了在数据抽象中所引入的数据
上的抽象算法与操作。在 Z 语言中，表示抽象通过类型定义、全局变量或常量以及状态空间
声明来进行表述；操作抽象通过函数和基于一阶谓词逻辑的操作来表述。
模式(schema)是Z语言的基本描述单位，它从软件系统的状态和状态之间的转化两个方
面来进行软件系统的描述。模式分为状态模式
和操作模式，状态模式定义了软件系统某一部分的状态空间及其约束特性，它通过相应抽象
数据类型的变量以及在它们上面所定义的一些约束关系来进行描述；操作模式则描述系统某
部分的行为特征，通过描述在操作之前的该部分的状态值与操作之后的该部分的状态值之间的关系，来定义该部分的某种操作的特性。
4.2 问题简介
实现一个多用户共享使用一台计算机的机制，每一个用户必须登录并且必须要有一
个口令 (password)。使用 Z 语言规格说明一个系统的登录与验证，必须保持注册过的用户
(Registered Users) 和他们的口令信息，而且必须跟踪当前系统中登录的活动的用户。具体来
说就是描述系统的状态、注册一个新的用户和口令、已经注册过的用户的登录、注销一个用户和它的口令，注意为该系统定义的许多操作
都将检查给定的用户是否已经注册。
4.3 给定类型
[User]：用户的集合
[Word]：用户口令的集合
[regd]：已经注册的用户的集合
[active]：已经登录的活动用户的集合
