软件工程复试——四、形式化说明技术

四、形式化说明技术

按照形式化的程度，可以把软件工程使用的方法划分为非形式化、半形式化、形式化三类。

（1）用自然语言描述需求规格说明是典型 的非形式化方法.

（2）用数据流图或E-R图建立的模型是典型 的半形式化方法。

（3）形式化方法是描述系统性质的基于数学 的技术，即如果一种方法有坚实的数学基础，那么它就是形式化的。

形式化方法的优点

• 准确、没有二义性
• 可以再软件工程活动之间平滑过渡
• 提供了高层确认的手段

应用形式化的准则：

1.选用适当的方法
2.应该形式化，但不要过度形式化
3.估算成本
4.有形式化方法顾问随时提供咨询
5.不应该放弃传统的方法
6.不应该放弃质量标准
7.不应该盲目以来形式化方法
8.反复测试
9.重用

有穷状态机

状态转换图

STD图(State Transform Diagram)状态转换图,表示行为模型。STD通过描述系统的状态和引起系统状态转换的事件，来表示系统的行为，指出作为特定事件的结果将执行哪些动作（例如，处理数据等）。STD描述系统对外部事件如何响应，如何动作。

各部分如下：

状态集、输入集、转换函数T、初始态S、终态集。

有穷训练机

具体例子各位可以看一下书上78、79页，这里光看概念不大行。

当前状态+事件+谓词==》下个状态

Petri

? Petri 是对离散并行系统的数学表示。Petri 是20世纪60年代由卡尔·A·佩特里发明的，适合于描述异步的、并发的计算机系统模型。 Petri 既有严格的数学表述方式，也有直观的图形表达方式，既有丰富的系统描述手段和系统行为分析技术，又为计算机科学提供坚实的概念基础。

? Petri 包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O

这个也是要在书上好好康康哦！

Z语言

? 形式化描述语言Z指的是著名数学家Zermelo，它是使用最广泛的一种形式化描述语言，在软件产业的一些大型项目中已经获得成功的应用，Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel，蔡梅罗-弗兰科尔）公理集合论为主要数学基础。

它主要有以下四部分组成：

• 给定的集合
• 状态定义
• 初始状态
• 操作

之所以Z语言会取得成功，原因如下（优点）

• 可以比较容易地发现用?Z?写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明?来审查设计与代码时，情况更是如此。
• Z?是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。
• 虽然完全学会?Z?语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写?Z?规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。?（学习简单）

课后题

1、

2、

在用非形式化的方式描述时，存在矛盾，二义性，含糊性，不完整性级抽象层次混乱等问题时用形式化说明技术。

• 应用形式化方法的准则：
• 应该选用适当的表示方法；
• 应该形式化，但不要过分形式化；
• 应该估算成本；
• 应该有形式化的方法顾问随时提供咨询；
• 不应该放弃传统的开发方式；
• 应该建立详尽的文档；
• 不应该放弃质量标准；
• 不应该盲目依赖形式化方法；
• 应该测试，测试再测试；
• 应该重用

（本章的知识有些零碎，并且有些地方比较难理解，各位一定要看书好好理解！！！感觉后面两个图和Z语言应该不是重点，大家看看即可