阅读第五章所了解到的基本知识，形式化方法是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动。主要目的是保证软件的正确性。已建立的形式化方法可分为操作类和描述类。操作类方法基于状态和转移;描述类基于数学公理和概念。形式证明与验证技术主要包括模型检测(适用于有穷状态系统,完全自动化并且验证速度快)和定理证明(采用逻辑公式来表示系统规约及其性质,分为自动和交互式两种)。一阶线性时态逻辑是一阶谓词逻辑的扩展。对汉诺塔操作规划问题有了更深一步的理解。计算树逻辑是一种离散、分支时间、命题时态逻辑。相比FOLTL増加了路径量词:所有未来路径、至少某一路径。Z语言的数学基础是集合论和—阶谓词演算,其模型的三个主要组成部分是输入、输出和状态。Z语言表示抽象的要素总体上可分为两类:基于集合理论的集合、关系、函数、序列和包,以及Z独有的模式。通过对Z语言实例的阅读，对Z语言有了进一步了解。Petri网分为位置/迁移Petri网和高级Petri网。Petri网具有丰富的结构描述能力,有顺序、并发、冲突、混惑结构模型。