第5章 软件工程中的形式化方法
从广义上讲，形式化方法（Formal Method）是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。将形式化方法运用于软件工程实践当中的只要目的是保证软件的正确性。
软件生命周期中的形式化转化策略：常用转化策略、直接转化策略和运用半形式化表示的中间转化策略。
进行模型化的过程中涉及到三种系统模型：现实世界、模型表示和计算机系统。
开发过程中的任务依次包括：模型获取、模型验证、模型变换。任务分别对应于三方面的活动：形式规约、形式证明与验证、程序求精。
一、形式化方法基本概念
软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。
当规格说明用非形式化方法描述时，可称之为“规格说明”，当规格说明用形式化方法描述时，可称之为“形式规约”。
从形式规约到目标软件系统的可实现和可执行角度，已建立的形式化方法可分为操作类和描述类。操作类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证，这类方法包括有险状态机、Statecharts、Petri网等。描述类方法基于数学公里和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点，便于通过自动工具进行验证。描述类的方法进一步分为：基于代数的方法，如Z、VDM、Larch等；基于逻辑的方法，如一阶线性时态逻辑（FOLTL）、计算树（CTL）逻辑等。
形式证明与验证技术主要包括模型检测和定理证明。
程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
程序求精的基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之间功能的一致性。
二、时态逻辑
Kripke结构 三元组M=（W，R，L）称为模态逻辑的一个模型，或者Kripke结构(模型)。
一阶线性时态逻辑（FOLTL）是一阶谓词逻辑的扩展。类似于PLTL，FOLTL是在一阶谓词逻辑中增加了模态词：必然、可能、下一时刻、直到。
计算树逻辑（CTL）是一种离散、分支时间、命题时态逻辑。
在CTL中，出了具有时态算子必然，可能，下一时刻，直到外，还增加了路径量词：所有未来路径（A）、至少某一路径（E）。
三、模型检测
四、Z语言
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态。Z语言形式规约由数学语言描述和自然语言注释两部分组成。
数据抽象和过程抽象是软件规格说明过程中的两类重要抽象。
集合是具有相同属性的元素构成的实体。
幂集 设A是一个集合，则由A的所有子集所组成的集合称为集合A的幂集，即为PA。通过使用一个基本类型和幂集构造符，即可产生一个新的类型，称为该基本类型的幂集类型。
远组合笛卡尔积。
关系和函数 一个序偶的集合称为二元关系。对于集合X和Y，用X↔Y表示X到Y的所有关系的集合，即X↔Y==Ρ（X×Y），并X为关系R的源集合，Y为关系R的目标集合。
队列和包 队列是有次序的对象的集合描述。包是描述数据对象的集合。
Z语言中，自由类型用于递归定义新类型。
模式是Z语言的基本描述单位。
五、Petri网
网状结构模拟通信系统这种系统模型以Petri网命名，Petri网又指以这种模型为基础发展起来的理论。
任何系统都可抽象为两类元素：状态和事件。
Petri网具有丰富的结构描述能力，有顺序关系、并发关系、冲突关系和混惑关系。