软件工程中的形式化方法
形式化方法是将离散数学的方法用于解决软件工程里领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。基本概念有形式规约，形式证明
与验证，程序求精。
模态逻辑是经典命题逻辑和一维谓词逻辑的扩展形式。Kriple结构是模态逻辑的一个模型。时态逻辑中有一阶线性时态逻辑是一阶谓词逻辑的扩展，还有计算树逻辑，是一种离散，分支时间问题时态逻辑。
模型检测就是在软件系统的Kriple结构模型下，对CTL*公式给出的软件性质的正确性的验证。
Z语言的介绍， 它表示表示抽象的要素总体上可以分为两类：基于集合理论的集合，关系，函数，序列和包，yijiZ语言独有的模式。这些表示要素组成了Z语言的类型系统。
本章最后介绍了Petri网，在任何系统都可以抽象为两类元素状态和事件。 Petri网是一个三元组，其中库所集和变迁集市Petri网的基本成分，流关系是他们构造出来的。