软件工程导论(第4章).pptVIP

4.3.2 例子 1. 电梯按钮 EBf 电梯中楼层 f 的按钮；Fg 楼层g；Ff 楼层 f。 2. 楼层按钮 FBfu 第 f 楼层向上按钮； FBfd 第 f 楼层向下按钮； 用Z语言描述的、最简单的形式化规格说明含有下述4个部分： 给定的集合、数据类型及常数。 状态定义。 初始状态。 操作。 4.4 Z语言 4.4.1 简介 1. 给定的集合 一个Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电梯问题，给定的初始化集合称为Button，即所有按钮的集合，因此，Z规格说明开始于： 〔Button〕 2. 状态定义 一个Z规格说明由若干个“格(schema)”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，格S的格式如图4.12所示。 图4.12 Z格S的格式 在电梯问题中，Button有4个子集，即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。 图4.13描述了格Button_State，其中，符号P表示幂集(即给定集的所有子集)。约束条件声明，floor_buttons集与elevator_buttons集不相交，而且它们共同组成buttons集(在下面的讨论中并不需要floor_buttons集和elevator_buttons集，把它们放于图4.13中只是用来说明Z格包含的内容)。 图4.13Z格Button_State 3. 初始状态 抽象的初始状态是指系统第一次开启时的状态。对于电梯问题来说，抽象的初始状态为： Button_Init 〔Button_State｜pushed=Φ〕 上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。 4. 操作 如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。图4.14定义了操作Push_Button(按按钮)。 图4.14操作Push_Button的Z规格说明 操作的谓词部分，包含了一组调用操作的前置条件，以及操作完全结束后的后置条件。如果前置条件成立，则操作执行完成后可得到后置条件。但是，如果在前置条件不成立的情况下调用该操作，则不能得到指定的结果(因此结果无法预测)。 假设电梯到达了某楼层，如果相应的楼层按钮已经打开，则此时它会关闭；同样，如果相应的电梯按钮已经打开，则此时它也会关闭。也就是说，如果“button?”属于pushed集，则将它移出该集合，如图4.15所示(符号“＼”表示集合差运算)。 图4.15操作Floor_Arrival的Z规格说明 已经在许多软件开发项目中成功地运用了Z语言，目前，Z也许是应用得最广泛的形式化语言，尤其是在大型项目中Z语言的优势更加明显。Z语言之所以会获得如此多的成功，主要有以下几个原因： (1) 可以比较容易地发现用Z写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。 (2) 用Z写规格说明时，要求作者十分精确地使用Z说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。 4.4.2 评价 (3) Z是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。 (4) 虽然完全学会Z语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。 (5) 使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。 (6) 虽然用户无法理解用Z写的规格说明，但是，可以依据Z规格说明用自然语言重写规格说明。经验证明，这样得到的自然语言规格说明，比直接用自然语言写出的非形式化规格说明更清楚、更正确。 使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。 小结 基于数学的形式化说明技术，目前还没有在软件产业界广泛应用； 应该把形式化方法与传统方法有机结合。 第三、四章练习题 填空题： 1、需求分析过程应该建立3种模型，它们分别是（ ）、（ ）和（ ）。 2、按照形式化的程度，可以把软件工程使用的方法划分成（ ）、（ ）和（ ）等3类。 3、验证软件