第五章软件工程中的形式化方法，本章的名字就让人摸不着头脑，还好在开篇的时候提到了离散数学，对于离散数学并不陌生，也让我能好好地读下去。
通读下来，本章我觉得主要针对的是软件的测试。
开始的时候是软件测试中的理论部分，用到了离散数学中的逻辑推理，其中拿出了汉诺塔、计算树逻辑进行了详细分析，将理论与现实更好的结合在一起，有助于读者的理解。
模型检测中提出了一个很重要的语言：Z语言，强调输入、过程、以及输出。拿出了停车场和图书管理系统做了介绍，这里建议读者学习一下离散数学以及统一建模方面的书籍，可以更好的帮助读者理解，从这了也可以更好的看出本章的内容，就是对于软件的测试。
petri网就是对于某个状态的测试，他可以针对某个状态进行检测，看看出的结果是不是能达到预想。
总体的看出来本章有针对状态和整体的测试，所以针对的是软件的测试。