本章主要讲述软件工程中将离散数学的方法用于解决软件工程领域的问题。形式化方法的开发可以追溯到20世纪50年代后期对编译技术的研究。也可以理解为，软件开发实际上就是把现实世界的需求映射成软件的模型化过程。
形式规约：软件规格说明是对软件系统对象，队象的操作方法，以及对象行为的描述。非形式的规格说明可用自然语言，图，表等形式描述。
形式证明与验证：主要包括模型检测和定理证明。
程序求精：将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
Z语言为以集合论和一阶谓词演算为数学基础的一种形式语言，为系统建立基于状态模型。主要为输入，输出和状态。
Z语言与离散数学有相似程度。