第五章 软件工程中的形式化方法
主要介绍了形式化方法的基本概念，时态逻辑，模型检验，Z语言和Petri网。
将形式化方法运用于软件工程实践当中的主要目的是保证软件的正确性。已建立的形式化方法可分为操作类和描述类。操作类方法基于状态和转移;描述类基于数学公理和概念。形式证明与验证技术主要包括模型检测和定理证明。一阶线性时态逻辑是一阶谓词逻辑的扩展。计算树逻辑是一种离散、分支时间、命题时态逻辑。Z语言的数学基础是集合论和—阶谓词演算,其模型的三个主要组成部分是输入、输出和状态。Z语言表示抽象的要素总体上可分为两类:基于集合理论的集合、关系、函数、序列和包,以及Z独有的模式。Petri网分为位置/迁移Petri网和高级Petri网。Petri网具有丰富的结构描述能力,有顺序、并发、冲突、混惑结构模型。