形式化说明技术.pptx

《形式化说明技术.pptx》由会员分享，可在线阅读，更多相关《形式化说明技术.pptx（62页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、4.1概述非形式化方法的缺点非形式化是指用自然语言描述软件需求（如系统规格说明书）。因此，可能存在矛盾性、二义性、含糊性、不完整性、抽象层次混乱等问题。形式化方法的优点形式化方法是指在软件工程中引入数学方法和模型。利用数学的简洁性、严谨性、科学性，克服非形式化方法的缺点。应用形式化方法的准则“软件需求”是软件产品的高层、概念模型，而“形式化方法”是严谨、科学的数学方法，因此，在形式化方法的应用方面应考虑适度性、实用性、实用性。常用的形式化方法较严格的形式化方法（语法和语义都严谨）：有穷状态机、Petri网、Z语言半形式化方法（语法和语义都不太严谨）：系统流程图、数据流图、数据字典、ER图、数据

2、库范式、状态转换图、层次方框图、Warnier图、IPO图、IPO表第1页/共62页非形式化方法的缺点矛盾性在需求规格说明书（Reqirement Specifications）中对同一问题前后存在不同的描述。二义性需求规格说明书的读者对其中同一问题的描述存在不同的理解。含糊性需求规格说明书中对某一问题的描述不清晰、不可理解、不知如何实现、不具可操作性。不完整性需求规格说明书中对某一问题的描述不完整。只说明了局部，没有说明整体；或者只说明了概要，未说明细节。因此不具可操作性。抽象层次混乱在不同层次的抽象模型中内容混乱，如在高层模型中混有底层细节，造成读者不能理解系统的整体功能和下级功能。第2页

3、/共62页形式化方法的优点可严谨地描述软件需求中的问题可简洁、准确描述物理现象、对象或动作的结果问题；适用于描述详细的需求规格；可用数学方法验证需求。可在软件工程不同阶段平滑过渡从需求、到设计、到实现都基于同一系统模型，平滑过渡。可提供高层确认手段可用数学方法证明软件工程各阶段的正确性（可回溯性），如“设计”符合“规格说明”、“编码实现”符合“设计”。形式化方法的适用性问题形式化方法能较好地解决需求的“二义性”、“含糊性”问题。但不能解决需求的矛盾性、完整性等问题，这些问题涉及工程管理。第3页/共62页应用形式化方法的准则应该选用适当的规格说明表示方法应该形式化，但不要过分形式化应该估算推行形

4、式化的成本应该有形式化方法顾问随时提供咨询应该结合传统的、证明有效的开发方法应该在采用形式化的同时，建立详尽的文档应该坚持质量保障活动应该不总是盲目依赖形式化方法应该重视测试应该重视重用第4页/共62页4.2有穷状态机有穷状态机概念有穷状态机例子有穷状态机方法评价第5页/共62页有穷状态机概念通过简单例子引入有穷状态机的基本概念：一个保险箱上装了一个复合锁，锁有三个位置，分别标记为 1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有 6 种可能的运动，即 1L、1R、2L、2R、3L 和 3R。保险箱的组合密码是 1L、3R、2L，转盘的任何其他运动都将引起报警。第6页/共

5、62页引例保险箱的状态转换图 4.1 保险箱的状态转换图 第7页/共62页引例保险箱的状态转换第8页/共62页有穷状态机概念一个有穷状态机包括下述 5 个部分：状态集 J、输入集 K、由当前状态和当前 输入确定下一个状态(次态)的转换函数T、初始态 S 和 终态集 F。状态集 J：由所有可能的状态构成的有穷集合；输入集 K：引发状态变换的可能的外部输入（或操作）；转换函数T：由当前状态和当前 输入变换到下一个状态(次态)的函数（或规则）；初始态 S J，状态机的初始状态；终态集 F J，状态机的终止状态集；第9页/共62页引例保险箱的有穷状态机状态集 J：保险箱锁定，A，B，保险箱解锁，报 警

6、。输入集 K：1L，1R，2L，2R，3L，3R。转换函数 T：见“状态转换表”初始态 S：保险箱锁定终态集 F：保险箱解锁，报警第10页/共62页有穷状态机形式化表示一个有穷状态机可以表示为一个 5 元组(J，K，T，S，F)，其中：J 是一个有穷的非空状态集；K 是一个有穷的非空输入集；T 是一个从(J-F)K 到 J 的转换函数；S J，是一个初始状态；F J，是终态集。第11页/共62页扩展的有穷状态机增加谓词集一个有穷状态机可以表示为一个 6 元组(J,K,P,T,S,F)，其中：J 是一个有穷的非空状态集；K是一个有穷的非空输入集；P是一个有穷的非空谓词集(条件函数集合)；T 是一

7、个从(J-F)KP 到 J 的转换函数；S J，是一个初始状态；F J，是终态集。第12页/共62页有穷状态机例子-电梯控制系统自然语言描述的对电梯系统的需求电梯系统有穷状态机-按钮集电梯按钮（电梯内）的状态转换楼层按钮（电梯外）的状态转换第13页/共62页自然语言描述的对电梯系统的需求在一幢 m 层的大厦中需要一套控制 n 部电梯的产品，要求这 n 部电梯按照约束条件 C1，C2 和 C3 在楼层间移动。C1：每部电梯内有 m 个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2：除了大厦的最低层和最高层之外，每层楼（电梯

8、外）都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。C3：当对电梯没有请求时，它关门并停在当前楼层。第14页/共62页电梯系统有穷状态机-按钮集现在使用一个扩展的有穷状态机对本产品进行规格说 明。这个问题中有两个按钮集：在n 部电梯中，每一部都 有 m 个按钮，一个按钮对应一个楼层。因为这 m n 个 按钮都在电梯中，所以称它们为电梯按钮。此外，每层楼有两个按钮（底楼、顶楼均只有一个），一个请求向上，另一个请求向下，这些按钮称为楼层按钮。第15页/共62页电梯按钮的状态转换（图）令 EB(e,f)表示按下电梯 e 内的按

9、钮并请求到 f 层去。EB(e,f)有两个状态，分别是按钮发光(打开)和不发光(关闭)，状态是：EBON(e,f)：电梯按钮(e,f)打开EBOFF(e,f)：电梯按钮(e,f)关闭 如果电梯按钮(e,f)发光且电梯到达 f 层，该按钮将熄灭。相反如果按钮熄灭，则按下它时，按钮将发光。上述描述中包含了两个事件，它们分别是：EBP(e,f)：电梯按钮(e,f)被按下 EAF(e,f)：电梯 e 到达 f 层第16页/共62页电梯按钮状态转换的相关谓词为了定义与这些事件和状态相联系的状态转换规则，需要一个谓词 V(e,f)，它的含义如下：V(e,f)：电梯 e 停在 f 层如果电梯按钮(e,f)处

10、于关闭状态当前状态，而且电梯按钮(e,f)被按下事件，而且电梯 e 不在 f 层谓 词，则该电梯按钮打开发光下个状态。状态转 换规则的形式化描述如下：EBOFF(e,f)+EBP(e,f)+not V(e,f)=EBON(e,f)反之，如果电梯到达 f 层，而且电梯按钮是打开的，于是它就会熄灭。这条转换规则可以形式化地表示为：EBON(e,f)+EAF(e,f)=EBOFF(e,f)第17页/共62页楼层按钮的状态转换（图）令 FB(d,f)表示 f 层请求电梯向 d 方向运动的按钮，楼层按钮 FB(d,f)的状态转换图如图 所示。楼层按钮的状态如下：FBON(d,f)：楼层按钮(d,f)打开

11、 FBOFF(d,f)：楼层按钮(d,f)关闭如果楼层按钮已经打开，而且一部电梯到达 f 层，则 钮关闭。反之，如果楼层按钮原来是关闭的，被按下 后该按钮将打开。这段叙述中包含了以下两个事件。FBP(d,f)：楼层按钮(d,f)被按下EAF(1 n,f)：电梯 1 或 或 n 到达 f 层，其中 1 n 表示或为 1 或为 2 或为 n。第18页/共62页楼层按钮状态转换的相关谓词为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个谓词S(d,e,f)，它的定义如下。S(d,e,f)：电梯 e 停在 f 层并且移动方向由 d 确定为向上(d=U)或向下(d=D)或待定(d=N)。这个谓

12、词实际上是一个状态，形式化方法允许把事件和状态作为谓词对待。使用谓词 S(d,e,f)，形式化转换规则为：FBOFF(d,f)+FBP(d,f)+not S(d,1 n,f)=FBON(d,f)FBON(d,f)+EAF(1 n,f)+S(d,1 n,f)=FBOFF(d,f)；其中,d=U or D。也就是说:如果在 f 层请求电梯向 d 方向运动的楼层按钮处于关闭状态，现在该按钮被按下，并且当时没有正停在 f 层准备向 d 方向移动的电梯，则该楼层按钮打开。反之，如果楼层按钮已经打开，且至少有一部电 梯到达 f 层，且该部电梯将朝 d 方向运动，则按钮将关闭。第19页/共62页V(e,f)

13、重新定义讨论电梯按钮状态转换规则时定义的谓词 V(e,f)（电梯e停在f层），可以用谓词 S(d,e,f)重新定义如下：V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)第20页/共62页电梯的状态、事件及转换规则电梯的 3 个状态：M(d,e,f)：电梯 e 正沿 d 方向移动，即将到达的是第 f 层 S(d,e,f)：电梯 e 停在 f 层，将朝 d 方向移动(尚未关门)W(e,f)：电梯 e 在 f 层等待(已关门)电梯的 3 个可触发状态发生改变的事件：DC(e,f)：电梯 e 在楼层 f 关上门ST(e,f)：电梯 e 靠近 f 层时触发传感器，电梯控制器决定

14、在当前楼层电梯是否停下RL：电梯按钮或楼层按钮被按下进入打开状态电梯的状态转换规则(这里给出的规则仅发生在关门之时)：S(U,e,f)+DC(e,f)=M(U,e,f+1)：如果电梯 e 停在 f 层准备向上(U)移动，且门已经关闭，则电梯将向上一楼层移动。S(D,e,f)+DC(e,f)=M(D,e,f-1)如果电梯 e 停在 f 层准备向下(D)移动，且门已经关闭，则电梯将向下一楼层移动。S(N,e,f)+DC(e,f)=W(e,f)。如果电梯 e 停在 f 层没有移动请求(N)，且门已经关闭，则电梯等待移动。第21页/共62页电梯的状态转换图 电电梯梯上上行行中中电电梯梯下下行行中中电梯

15、等待中电梯等待中电梯被控电梯被控第22页/共62页有穷状态机方法评价（特点）采用一种简单的有穷状态机方法格式 来描述规格说明：当前状态+事件+谓词=下个状态这种形式的规格说明易于书写、易于验证。有穷状态机可以比较容易地把它转变成设计或程序代码：可开发一个 CASE 工具把一个有穷状态机规格说明直接 转变为源代码。维护可以通过重新转变来实现，也就是说，如果需要一个新的状态或事件，首先修改规格 说明，然后直接由新的规格说明生成新版本的产品。有穷状态机方法与数据流图技术比较有穷状态机描述需求比数据流图技术更精确；与数据流图一 样易于理解（还是要难一点）。有穷状态机存在的缺点：在开发一个大系统时三元组

16、(即状态、事件、谓词)的数量会迅速增长。和数据流图方法一样，形式化的有穷状态机方法 也没有处理定时需求。（下节将介绍的 Petri 网技术，是一种可处理定时问题的形式化方法。）第23页/共62页4.3Petri网网概念网例子网方法评价第24页/共62页网概念软件系统的定时问题Petri网及其用途Petri网的构成Petri网的形式化表示第25页/共62页软件系统的定时问题并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式，如同步问题、竞争条件以及死锁问题。定时出现问题通常是由不好的设计或有错误的实现引起的，而这样的设计或实现通常又是由不好的规格说明造成的。如果规格说明不恰当，则

17、有导致不完善的设计或实现的危险。第26页/共62页Petri网及其用途用于确定系统中隐含的定时问题的一种有效技术是 Petri 网，这种技术的一个很大的优点是它也可以用于设计中，有效地描述并发活动。Petri网是对离散并行系统的数学表示。Petri网既有严格的数学表述方式，也有直观的图形表达方式。Petri网适合于描述异步的、并发的自动化系统和计算机系统模型。Petri 网在计算机科学中得到了广泛的应用，例如，在系统性能评价、操作系统和软件工程等领域，Petri 网应用得都比较广泛。第27页/共62页Petri网的构成Petri 网包含 4 种元素：一组位置 P(Place):圆圈一组转换 T

18、(Transition):短直线 输入函数 I(Input)输出函数 O(Output)其他元素连接Connection:箭头权标Token(令牌):圆点例P:P1,P2,P3,P4T:t1,t2 I:I(t1)=P2,P4,I(t2)=P2O:O(t1)=P1 O(t2)=P3，P3 第28页/共62页Petri网的形式化表示一个Petri网是一个四元组CC=(P,T,I,O)其中:P=P1，Pn 是一个有穷位置集，n 0。T=t1，tm 是一个有穷转换集，m 0，且 T 和 P 不相交。I：T P 为输入函数，是由转换到位置无序单位组(bags)的映射。O：T P 为输出函数，是由转换到位

19、置无序单位组的映射。一个无序单位组（或多重组）是允许一个元素有多个实例的广义集第29页/共62页Petri网的标记权标(token，令牌)Petri网位置P中的权标（用圆点表示），表示该位置持有的可激发与其连接的后继转换t的条件。标记（M，Mark）Petri网的标记是在Petri网中权标(token，令牌)的分配。Petri 网 标记M 是由一组位置 P 到一组非负整数的映射，即M：P 0，1，2，其中的数字表示每个位置中当前的权标数量。转换的激发通常，当每个输入位置所拥有的权标数大于等于从该位置到所直接连接的后续转换 t 的线数时，就允许激发该转换 t。此时，t所直接连接的前序位置减少一个

20、权标（用掉了1个）；t所直接连接的后续位置增加一个权标（获得了1个）。Petri 网具有非确定性，也就是说，如果数个转换 都达到了激发条件，则其中任意一个都可以被激发。第30页/共62页例：带权标的Petri网在图 4.6 中有 4 个权标，其中一个在 P1 中，两个在 P2 中，P3 中没有，还有一个在 P4 中。上述标记可以用向量(1,2,0,1）表示。由于P2 和 P4 中有权标，因此 t1 启动(即被激发)。当 t1 被激发 时，P2 和 P4 上各有一个权标被移出，而 P1上则增加一个权标。Petri 网中权标总数不是固定的，在这个例子中两个权标被移出，而 P1 上只能增加一个权标。

21、图4.6 带标记的Petri网图4.7 Petri网在转换t1被激发后的情况第31页/共62页例：带权标的Petri网（续）在图 4.6 中 P2 上有权标，因此 t2 也可以被激发。当 t2 被激发时，P2 上将移走一个权标，而 P3 上新增加两个权 标。图 4.6 所示 Petri 网的标记为(1，2，0，1)，t1 和 t2 都可以被激发。假设 t1 被激发了，则结果如图 4.7 所示，标记为(2，1，0，0)。此时，只有 t2 可以被激发。如果 t2 也 被激发了，则权标从 P2 中移出，两个新权标被放在 P3 上，结果如图 4.8 所示，标记为(2，0，2，0)。图4.7 Petri

22、网在转换t1被激发后的情况图4.8图4.7的Petri网在转换t2被激发后的情况第32页/共62页含禁止线的Petri网禁止线是使用“圆点”（而不是箭头）标记的输入线。表示禁止线上（图中P2）没有权标时，后续的转换（图中t1）才可激活。图4.9例：箭头线P3上有权标，而禁止线P2上没有权标，所以转换t1可以激活。图4.9含禁止线的Petri网第33页/共62页更形式化的Petri网定义（增加标记M）一个Petri网是一个五元组CC=(P，T，I，O，M)其中:P=P1，Pn 是一个有穷位置集，n 0。T=t1，tm 是一个有穷转换集，m 0，且 T 和 P 不相交。I：T P 为输入函数，是由

23、转换到位置无序单位组(bags)的映射。O：T P 为输出函数，是由转换到位置无序单位组的映射。M：P0，1，2，是由一组位置P到一组非负整数的映射第34页/共62页网例子：电梯系统控制Petri网应用于电梯问题当用Petri网表示上一节讨论过的电梯系统的规格说明时，每个楼层用一个位置Ff代表(1fm)；在Petri网中电梯是用一个权标代表的。在位置Ff上有权标，表示在楼层f上有电梯。可能的几种约束条件电梯按钮（约束条件C1，电梯内有按钮操作）楼层按钮（约束条件C2，楼层中有按钮操作）电梯静止（约束条件C3，没有任何操作请求）第35页/共62页1.电梯按钮（约束条件C1）第一个约束条件C1，描

24、述了“电梯按钮”的行为：每部电梯有m个按钮，每层对应一个按钮。当按下一个按钮时该按钮指示灯亮，指示电梯移往相应的楼层。当电梯到达指定的楼层时，按钮将熄灭。为了用Petri网表达电梯按钮的规格说明，在Petri网中还必须设置其他的“电梯按钮位置”：电梯中楼层f的按钮，在Petri网中用位置EBf表示(1fm)在EBf上有一个权标，就表示电梯内楼层f的按钮被按下了。电梯按钮只有在第一次被按下时才会由暗变亮，以后再按它则只会被忽略。第36页/共62页电梯按钮的 Petri网图4.10所示的Petri网准确地描述了电梯按钮的行为规律：首先，假设按钮没有发亮，显然在位置EBf上没有权标，从而在存在禁止线

25、的情况下，转换“EBf被按下”是允许发生的。假设现在按下按钮，则转换被激发并在EBf上放置了一个权标。以后不论再按下多少次按钮，禁止线与现有权标的组合都决定了转换“EBf被按下”不能再被激发了，因此，位置EBf上的权标数不会多于1。图4.10 Petri网表示的电梯按钮第37页/共62页电梯按钮的 Petri网（续）续：假设电梯由g层驶向f层，因为电梯在g层，位置Fg 有一个权标。由于每条输入线上各有一个权标，转换“电梯在运行”被激发，从而EBf和Fg上的权标被移走，按钮Bf关闭，在位置 Ff 上出现一个新权标，即转换的激发使电梯由 g 层驶到 f 层。事实上，电梯由g层移到f层是需要时间的，

26、为处理这个情况及其他类似的问题(例如，由于物理上的原因按钮被按下后不能马上发亮)，Petri网模型中必须加入时限。也就是说，在标准Petri网中转换是瞬时完成的，而在现实情况下就需要时间控制Petri网，以使转换与非零时间相联系。图4.10 Petri网表示的电梯按钮第38页/共62页2.楼层按钮（约束条件C2）第二条约束C2，描述了楼层按钮的行为：除了第一层与顶层之外，每个楼层都有两个按钮，一个要求电梯上行，另一个要求电梯下行。这些按钮在按下时发亮，当电梯到达该层并将向指定方向移动时，相应的按钮才会熄灭。在Petri网中楼层按钮位置：Petri网中楼层按钮用位置FBfu和FBfd表示，分别代

27、表f楼层请求电梯上行和下行的按钮。底层的按钮为FB1u，最高层的按钮为FBmd，中间每一层有两个按钮FBfu和FBfd(1fm)。第39页/共62页楼层按钮的Petri网（图）图4.11 Petri网表示楼层按钮第40页/共62页楼层按钮的Petri网图4.11所示的情况为电梯由g层驶向f层。根据电梯乘客的要求，某一个楼层按钮亮或两个楼层按钮都亮。如果两个按钮都亮了，则只有一个按钮熄灭。图4.11所示的Petri网可以保证，当两个按钮都亮了的时候，只有一个按钮熄灭。但是要保证按钮熄灭正确，则需要更复杂的Petri网模型。第42页/共62页第41页/共62页电梯静止条件（约束条件C3）最后，考虑

28、第三条约束C3：当电梯没有收到请求时，它将停留在当前楼层并关门。这条约束很容易实现，如下图所示，当没有请求(FBfu和FBfd上无权标）时，任何一个转换“电梯在运行”都不能被激发，而是停留在当前层（Fg）。第42页/共62页网方法评价Petri网是1960年代由C.A.佩特里发明的，Petri网是对离散并行系统的数学表示。Petri网适合于描述异步的、并发的计算机系统模型。Petri网既有严格的数学表述方式，也有直观的图形表达方式。由于Petri网能表达并发的事件，被认为是自动化理论的一种。研究领域趋向认为Petri网是所有流程定义语言之母。第43页/共62页4.4Z语言语言简介语言例子语言评

29、价第44页/共62页Z语言简介Z语言是由牛津大学程序设计研究小组开发的一种描述形式语言，在ISO指导下的国际标准化Z工作于2002年完成。Z语言中的“Z”指的是著名数学家Zermelo。Z语言是目前使用最广泛的一种形式化描述语言，Z语言将事物的状态和行为用数学符号形式化表达的语言，为编写计算机程序和验证计算机程序的正确性提供依据，是软件工程中编码之前的规格说明语言。Z语言在软件产业的一些大型项目中已经获得成功的应用，。Z语言是一种以一阶谓词演算为主要理论基础的规约语言,是一种功能性语言。Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel，蔡梅罗-弗兰科尔）公理集合论为主要数学基础。

30、在Z中有两种语言：数学语言和模式（Schema）语言。数学语言用来描述系统的各种特征：对象及其之间的关系。模式语言是一种半图形化的语言，它用来构造、组织形式化说明的描述、整理、封装信息块并对其命名以便可以重用这些信息块。通常，形式化说明的可读性都不太好，但由于Z采用半图形化的模式语言，能用一种比较直观、有条理的方式来表达形式化说明，这就改善了可读性。第45页/共62页Z语言的需求规格说明的构成用Z语言描述的、最简单的形式化规格说明含有下述4个部分：给定的集合、数据类型及常数。状态定义。初始状态。操作。第46页/共62页1.给定的集合给定的集合一个Z规格说明从一系列给定的初始化集合开始。所谓初始

31、化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。电梯控制系统的“给定的集合”电梯问题中给定的初始化集合称为Button，即所有按钮的集合，因此，Z规格说明开始于：Button第47页/共62页2.状态定义状态定义Z格一个Z规格说明由若干个“格(schema)”组成，Z格的格式如图4.12所示。Z格由以下几个部分构成：格的名称（如：“S”）；一组说明（Declarations），给出Z格中可能用到的变量；一组谓词（Predicates），限定变量取值范围的。图4.12 Z格S的格式第48页/共62页电梯控制系统中的Z格：Button_State（图）图4.13 Z格Button_S

32、tate 变量说明（集合）谓词（约束条件）第49页/共62页电梯控制系统中的Z格：Button_State电梯系统Z格中的说明Button有4个子集：floor_buttons(楼层按钮的集合)elevator_buttons(电梯按钮的集合)buttons(电梯问题中所有按钮的集合)pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。符号P表示幂集(即给定集的所有子集)(在下面的讨论中并不需要floor_buttons集和elevator_buttons集，把它们放于图4.13中只是用来说明Z格包含的内容)电梯系统Z格中的谓词约束条件声明:floor_buttons集与el

33、evator_buttons集不相交;而且它们共同组成buttons集。第50页/共62页3.初始状态初始状态抽象的初始状态是指系统第一次开启时的状态。电梯控制系统的抽象初始状态为：Button_InitButton_Statepushed=上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。第51页/共62页4.操作Z规格说明中的操作描述了需求的操作，包括操作涉及到的变量、操作的前提（前置条件）以及操作的结果（后置条件）。操作的说明部分操作的说明部分定义了该操作涉及到的输入、输出变量。操作的谓词部分操作的谓词部分包含了一组调用操作的前置条件，以及操作完全结束后的后置条件。

34、如果前置条件成立，则操作执行完成后可得到后置条件。但是，如果在前置条件不成立的情况下调用该操作，则不能得到指定的结果(因此结果无法预测)。运算符&表达式格名在本格中引用的格；变量名？、变量名！输入变量、输出变量；逻辑运算符（、）；集合运算符（、）；变量名 变化后的变量。图4.14 操作Push_Button的Z规格说明第52页/共62页电梯控制系统的操作：Push_Button图4.14定义了“按下按钮”操作Push_Button如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。操作的说明部分该操作中引用了外部Z格 Button_State；该操作的输入变

35、量为Button？。操作的谓词部分第一个前置条件：输入变量 button？buttons（所有按钮的集合）；第二个前置条件：输入变量 button？不属于pushed，则在pushed集合中增加该按钮；第三个前置条件：输入变量 button？属于pushed，则pushed保持不变（操作前后状态一样）。如果没有该条件，后果无法预测！图4.14 操作Push_Button的Z规格说明第53页/共62页电梯控制系统的操作：Floor_Arrival操作Floor_Arrival假设电梯到达了某楼层，如果相应的楼层按钮已经打开，则此时它会关闭；同样，如果相应的电梯按钮已经打开，则此时它也会关闭。也就

36、是说，如果“button?”属于pushed集，则将它移出该集合，如图4.15。图4.15 操作Floor_Arrival的Z规格说明第54页/共62页评价使用形式化规格说明是全球的总趋势。目前，Z也许是应用得最广泛的形式化语言，尤其是在大型项目中Z语言的优势更加明显。已经在许多软件开发项目中成功地运用了Z语言。Z语言之所以会获得如此多的成功，有诸多的原因和特点（下页）。第55页/共62页Z语言的主要优点及特点(1)易于发现规格说明中的错误可以比较容易地发现用Z写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。(2)可精确地描述规格说明用Z写

37、规格说明时，要求作者十分精确地使用Z说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。(3)方便需求说明的正确性验证Z是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。(4)具有一定的可掌握性虽然完全学会Z语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。(5)可降低软件开发费用使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。(6)易于正确地转换成自然语言描述虽然用户

38、无法理解用Z写的规格说明，但是，可以依据Z规格说明用自然语言重写规格说明。经验证明，这样得到的自然语言规格说明，比直接用自然语言写出的非形式化规格说明更清楚、更正确。第56页/共62页Z语言参考资料第57页/共62页4.5小结形式化规格说明方法的优点基于数学的形式化规格说明技术，与欠形式化的方法比较起来，它确实有实质性的优点：形式化的规格说明可以用数学方法研究、验证(例如，一个正确的程序可以被证明满足其规格说明，两个规格说明可以被证明是等价的，规格说明中存在的某些形式的不完整性和不一致性可以被自动地检测出来)。此外，形式化的规格说明消除了二义性，而且它鼓励软件开发者在软件工程过程的早期阶段使用

39、更严格的方法，从而可以减少差错。形式化规格说明方法的缺点形式化方法也有缺点：大多数形式化的规格说明主要关注于系统的功能和数据，而问题的时序、控制和行为等方面的需求却更难于表示。此外，形式化方法比欠形式化方法更难学习，不仅在培训阶段要花大量的投资，而且对某些软件工程师来说，它代表了一种“文化冲击”。形式化方法和欠形式化方法结合把形式化方法和欠形式化方法有机地结合起来，使它们取长补短，应该能获得更理想的效果。本章讲述的应用形式化方法的准则(见节)，对于读者今后在实际工作中更好地利用形式化方法，可能是有帮助的。第58页/共62页习题 44-1 举例对比形式化方法和欠形式化方法的优缺点。4-2 在什么

40、情况下应该使用形式化说明技术?使用形式化说明技术时应遵守哪些准则?4-3 一个浮点二进制数的构成是：一个可选的符号(+或-)，后跟一个或多个二进制位，再跟上一个字符E，再加上另一个可选符号(+或-)及一个或多个二进制位。例如，下列的字符串都是浮点二进制数：110101E-101-100111E11101+1E0更形式化地，浮点二进制数定义如下：floatingpoint binary=signbitstringEsignbitstringsign=+-bitstring=bitbitstringbit=01其中，符号=表示定义为；符号.表示可选项；符号ab表示a或b。假设有这样一个有穷状态机：

41、以一串字符为输入，判断字符串中是否含有合法的浮点二进制数。试对这个有穷状态机进行规格说明。第59页/共62页习题 4（续）4-4 考虑下述的自动化图书馆流通系统：每本书都有一个条形码，每个借阅人都有一个带有条形码的卡片。当一个借阅人想借一本书时，图书管理员扫描书上的条形码和借阅人卡片上的条形码，然后在计算机终端上输入C；当归还一本书时，图书管理员将再做一次扫描，并输入R。图书管理员可以把一些书加到(+)图书集合中，也可以删除(-)它们。借阅人可以在终端上查找到某个作者所有的书(输入“A=”和作者名字)，或具有指定标题的所有书籍(输入“T=”和标题)，或属于特定主题范围内的所有图书(输入“S=”加主题范围)。最后，如果借阅人想借的书已被别人借走，图书管理员将给这本书设置一个预约，以便书归还时把书留给预约的借阅人(输入“H=”加书号)。试用有穷状态机说明上述的图书流通系统。4-5 试用Petri网说明第4题所述图书馆中一本书的循环过程。在规格说明中应该包括操作H、C及R。4-6 试用Z语言对第4题所述图书馆图书流通系统做一个完整的规格说明。第60页/共62页The END第61页/共62页感谢您的观看！第62页/共62页