第4章软件工程.ppt

《第4章软件工程.ppt》由会员分享，可在线阅读，更多相关《第4章软件工程.ppt（64页珍藏版）》请在三一文库上搜索。

1、2019/6/4,湖南科技大学 计算机学院 戴祖雄,1,第4章 形式化说明技术,教学目标及基本要求 : 1.了解形式化与非形式化的区别 2.了解应用形式化方法的准则 3.掌握有穷状态机 4.掌握Petri网 5.掌握Z语言,教学重点: 1.有穷状态机 2.Petri网,学时数：2课时,教学难点: 有穷状态机和Petri网的具体应用,2019/6/4,湖南科技大学 计算机学院 戴祖雄,2,习题 : 1 举例对比形式化方法和欠形式化方法的优缺点。 2 在什么情况下应该使用形式化说明技术?使用形式化说明技术时应遵守哪些准则? 3 考虑下述的自动化图书馆流通系统：每本书都有一个条形码，每个借阅人都有一

2、个带有条形码的卡片。当一个借阅人想借一本书时，图书管理员扫描书上的条形码和借阅人卡片上的条形码，然后在计算机终端上输入C；当归还一本书时，图书管理员将再做一次扫描，并输入R。图书管理员可以把一些书加到(+)图书集合中，也可以删除(-)它们。 借阅人可以在终端上查找到某个作者所有的书(输入“A=”和作者名字)，或具有指定标题的所有书籍(输入“T=”和标题)，或属于特定主题范围内的所有图书(输入“S=”加主题范围)。最后，如果借阅人想借的书已被别人借走，图书管理员将给这本书设置一个预约，以便书归还时把书留给预约的借阅人(输入“H=”加书号)。 试用有穷状态机说明上述的图书流通系统。,2019/6/

3、4,湖南科技大学 计算机学院 戴祖雄,3,教学内容 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结,2019/6/4,湖南科技大学 计算机学院 戴祖雄,4,第4章 形式化说明技术,根据形式化的程度,可以把软件工程方法划分成非形式化、半形式化和形式化三类。使用自然语言描述需求规格说明,是典型的非形式化方法。使用数据流图或实体关系图等图形符号建立模型,是典型的半形式化方法。 用于开发计算机系统的形式化方法,是描述系统性质的基于数学的技术,也就是说,如果一个方法有坚实的数学基础,那么它就是形式化的。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,5,4.1

4、 概述,4.1.1 非形式化方法的缺点 基本上使用自然语言描述的系统规格说明,可能存在矛盾、二义性、含糊性、不完整性以及抽象层次混杂等问题。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,6,4.1.2 形式化方法的优点 数学最有用的性质之一是,它能够简洁、准确地描述物理现象、对象或动作的结果,因此是理想的建模工具。 在软件开发过程中使用数学的另一个优点是,可以在软件工程活动之间平滑地过渡。不仅功能规格说明,而且系统设计也可以用数学表达,当然,程序代码也是一种数学符号。 数学作为软件开发工具的最后一个优点是,它提供了高层确认的手段。可以使用数学方法证明,设计符合规格说明,程序代码正确地反

5、映了设计结果。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,7,4.1.3 应用形式化方法的准则 应用形式化方法的几条准则: 选择适用于当前项目的符号系统。 应该形式化,但不要过分形式化。 应该进行成本/效益分析。 需要有形式化方法的顾问。 不要放弃传统的开发方法。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,8,应该建立详尽的文档。 不应该放弃质量标准。 不应该盲目依赖形式化方法。 应该测试、测试再测试。 应该重用。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,9,4.2 有穷状态机,利用有穷状态机可以准确地描述一个系统,因此是表达规格说明的一种形式化方法。 4.2.

6、1 基本概念 下面通过一个简单例子介绍有穷状态机的基本概念。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,10,一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。图4.1描绘了保险箱的状态转换情况。 图4.1是一个有穷状态机的状态转换图。状态转换并不一定要用图形方式描述，表4.1的表格形式也可以表达同样的信息。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,11,图4.1 保险箱的状态转换

7、图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,12,2019/6/4,湖南科技大学 计算机学院 戴祖雄,13,从上面这个简单例子可以看出,一个有穷状态机包括下述5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 如果使用更形式化的术语,一个有穷状态机可以表示为一个5元组(J,R,T,S,F),其中： J是一个有穷的非空状态集； K是一个有穷的非空输入集； T是一个从(J-F)K到J的转换函数； SJ,是一个初始状态； FJ,是终态集。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,14,当前状态菜单+事件所选择的项下个状态

8、 为了对一个系统进行规格说明,通常都需要对有穷状态机做一个很有用的扩展,即在前述的5元组中加入第6个组件谓词集P,即把有穷状态机扩展为一个6元组,其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)KP到J的函数。现在的转换规则形式如下： 当前状态菜单+事件所选择的项+谓词下个状态,2019/6/4,湖南科技大学 计算机学院 戴祖雄,15,4.2.2 例子(电梯问题) 电梯按钮的状态转换图如图4.2所示。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态,分别是按钮发光(打开)和不发光(关闭)。更精确地说,状态是: EBON(e,f)：电梯按钮(e

9、,f)打开 EBOFF(e,f)：电梯按钮(e,f)关闭 如果电梯按钮(e,f)发光且电梯到达f层,该按钮将熄灭。相反如果按钮熄灭,则按下它时,按钮将发光。上述描述中包含了两个事件,它们分别是：,2019/6/4,湖南科技大学 计算机学院 戴祖雄,16,图4.2 电梯按钮的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,17,EBP(e,f)：电梯按钮(e,f)被按下 EAF(e,f)：电梯e到达f层 为了定义与这些事件和状态相联系的状态转换规则,需要一个谓词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),2019/6/4,湖南科技大学 计算机学院 戴祖雄,18,接下来让我们考虑楼层按钮。令FB(d,f)表示f层的按钮请求电梯向d方向运动,楼层按钮FB(d,f)的状态转换图如图4.3所示。 楼层按钮的状态如下: FBON(d,f)：楼层按钮(d,f)打开； F

11、BOFF(d,f)：楼层按钮(d,f)关闭。 如果楼层按钮已经打开,而且一部电梯到达f层,则按钮关闭。反之,如果楼层按钮原来是关闭的,被按下后该按钮将打开。这段叙述中包含了以下两个事件: FBP(d,f)：楼层按钮(d,f)被按下 EAF(1n,f)：电梯1或或n到达f层 其中1n表示或为1或为2或为n。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,19,图4.3 楼层按钮的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,20,为了定义与这些事件和状态相联系的状态转换规则,同样也需要一个谓词,它是S(d,e,f),它的定义如下。 S(d,e,f)：电梯e停在f层并且移动

12、方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)。 这个谓词实际上是一个状态,形式化方法允许把事件和状态作为谓词对待。 使用谓词S(d,e,f),形式化转换规则为： FBOFF(d,f)+FBP(d,f)+not S(d,1n,f)FBON(d,f) FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f) 其中,d=UorD。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,21,也就是说,如果在f层请求电梯向d方向运动的楼层按钮处于关闭状态,现在该按钮被按下,并且当时没有正停在f层准备向d方向移动的电梯,则该楼层按钮打开。反之,如果楼层按钮已经打开,且

13、至少有一部电梯到达f层,该部电梯将朝d方向运动,则按钮将关闭。 在讨论电梯按钮状态转换规则时定义的谓词V(e,f),可以用谓词S(d,e,f)重新定义如下： V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f),2019/6/4,湖南科技大学 计算机学院 戴祖雄,22,下面定义电梯的三个状态： M(d,e,f)：电梯e正沿d方向移动,即将到达的是第f层； S(d,e,f)：电梯e停在f层,将朝d方向移动(尚未关门)； W(e,f)：电梯e在f层等待(已关门)。 其中S(d,e,f)状态已在讨论楼层按钮时定义过,但是,现在的定义更完备一些。 图4.4是电梯的状态转换图。注意

14、,三个电梯停止状态S(U,e,f)、S(N,e,f)和S(D,e,f)已被组合成一个大的状态,这样做的目的是减少状态总数以简化流图。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,23,图4.4 电梯的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,24,图4.4中包含了下述三个可触发状态发生改变的事件: DC(e,f)：电梯e在楼层f关上门。 ST(e,f)：电梯e靠近f层时触发传感器,电梯控制器决定在当前楼层电梯是否停下。 RL：电梯按钮或楼层按钮被按下进入打开状态,登录需求。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,25,最后,给出电梯的状态转换规则。为

15、简单起见,这里给出的规则仅发生在关门之时。 S(U,e,f)+DC(e,f)M(U,e,f+1) S(D,e,f)+DC(e,f)M(D,e,f-1) S(N,e,f)+DC(e,f)W(e,f) 第一条规则表明,如果电梯e停在f层准备向上移动,且门已经关闭,则电梯将向上一楼层移动。第二条和第三条规则,分别对应于电梯即将下降或者没有待处理的请求的情况。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,26,4.2.3 评价 有穷状态机方法采用了一种简单的格式来描述规格说明： 当前状态+事件+谓词下个状态 这种形式的规格说明易于书写、易于验证,而且可以比较容易地把它转变成设计或程序代码。事实

16、上,可以开发一个CASE工具把一个有穷状态机规格说明直接转变为源代码。维护可以通过重新转变来实现,也就是说,如果需要一个新的状态或事件,首先修改规格说明,然后直接由新的规格说明生成新版本的产品。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,27,有穷状态机方法比数据流图技术更精确,而且和它一样易于理解。不过,它也有缺点：在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外,和数据流图方法一样,形式化的有穷状态机方法也没有处理定时需求。下节将介绍的Petri网技术,是一种可处理定时问题的形式化方法。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,28,4.3 Pet

17、ri网,4.3.1 基本概念 Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。图4.5举例说明了Petri网的组成。 其中: 一组位置P为P1,P2,P3,P4,在图中用圆圈代表位置。 一组转换T为t1,t2,在图中用短直线表示转换。 ,2019/6/4,湖南科技大学 计算机学院 戴祖雄,29,图4.5 Petri网的组成,2019/6/4,湖南科技大学 计算机学院 戴祖雄,30,两个用于转换的输入函数,用由位置指向转换的箭头表示,它们是： I(t1)=P2,P4 I(t2)=P2 两个用于转换的输出函数,用由转换指向位置的箭头表示,它们是： O(t1)=P1 O(

18、t2)=P3,P3 注意,输出函数O(t2)中有两个P3,是因为有两个箭头由t2指向P3。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,31,更形式化的Petri网结构,是一个四元组C=(P,T,I,O)。其中: P=P1,Pn是一个有穷位置集,n0。 T=t1,tm是一个有穷转换集,m0,且T和P不相交。 I：TP为输入函数,是由转换到位置无序单位组(bags)的映射。 O：TP为输出函数,是由转换到位置无序单位组的映射。 一个无序单位组或多重组是允许一个元素有多个实例的广义集。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,32,Petri网的标记是在Petri网中令牌(to

19、ken)的分配。例如,在图4.6中有4个令牌,其中一个在P1中,两个在P2中,P3中没有,还有一个在P4中。上述标记可以用向量(1,2,0,1)表示。由于P2和P4中有令牌,因此t1启动(即被激发)。通常,当每个输入位置所拥有的令牌数等于从该位置到转换的线数时,就允许转换。当t1被激发时,P2和P4上各有一个令牌被移出,而P1上则增加一个令牌。Petri网中令牌总数不是固定的,在这个例子中两个令牌被移出,而P1上只能增加一个令牌。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,33,在图4.6中P2上有令牌,因此t2也可以被激发。当t2被激发时,P2上将移走一个令牌,而P3上新增加两个令

20、牌。Petri网具有非确定性,也就是说,如果数个转换都达到了激发条件,则其中任意一个都可以被激发。图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)。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,34,图4.6 带标记的Petri网,2019/6/4,湖南科技大学 计算机学院 戴祖雄,35,图4.7 图4.6的Petri网在转换t1被激发后的情况,2019/6/4

21、,湖南科技大学 计算机学院 戴祖雄,36,图4.8 图4.7的Petri网在转换t2被激发后的情况,2019/6/4,湖南科技大学 计算机学院 戴祖雄,37,更形式化地说,Petri网C=(P,T,I,O)中的标记M,是由一组位置P到一组非负整数的映射： M：P0,1,2, 这样,带有标记的Petri网成为一个五元组(P,T,I,O,M)。 对Petri网的一个重要扩充是加入禁止线。如图4.9所示,禁止线是用一个小圆圈而不是用箭头标记的输入线。通常,当每个输入线上至少有一个令牌,而禁止线上没有令牌的时候,相应的转换才是允许的。在图14.9中,P3上有一个令牌而P2上没有令牌,因此转换t1可以被

22、激发。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,38,图4.9 含禁止线的Petri网,2019/6/4,湖南科技大学 计算机学院 戴祖雄,39,4.3.2 应用实例 让我们把Petri网应用于上一节讨论过的电梯问题。当用Petri网表示电梯系统的规格说明时,每个楼层用一个位置Ff代表(1fm),在Petri网中电梯是用一个令牌代表的。在位置Ff上有令牌,表示在楼层f上有电梯。 1.电梯按钮 为了用Petri网表达电梯按钮的规格说明,在Petri网中还必须设置其他的位置。电梯中楼层f的按钮,在Petri网中用位置EBf表示(1fm)。在EBf上有一个令牌,就表示电梯内楼层f的按钮被

23、按下了。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,40,电梯按钮只有在第一次被按下时才会由暗变亮,以后再按它则只会被忽略。图4.10所示的Petri网准确地描述了电梯按钮的行为规律。首先,假设按钮没有发亮,显然在位置EBf上没有令牌,从而在存在禁止线的情况下,转换“EBf被按下”是允许发生的。假设现在按下按钮,则转换被激发并在EBf上放置了一个令牌,如图4.10所示。以后不论再按下多少次按钮,禁止线与现有令牌的组合都决定了转换“EBf被按下”不能再被激发了,因此,位置EBf上的令牌数不会多于1。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,41,图4.10 Petri网表示

24、的电梯按钮,2019/6/4,湖南科技大学 计算机学院 戴祖雄,42,假设电梯由g层驶向f层,因为电梯在g层,如图4.10所示,位置Fg上有一个令牌。由于每条输入线上各有一个令牌,转换“电梯在运行”被激发,从而EBf和Fg上的令牌被移走,按钮EBf被关闭,在位置Ff上出现一个新令牌,即转换的激发使电梯由g层驶到f层。 事实上,电梯由g层移到f层是需要时间的,为处理这个情况及其他类似的问题(例如,由于物理上的原因按钮被按下后不能马上发亮),Petri网模型中必须加入时限。也就是说,在标准Petri网中转换是瞬时完成的,而在现实情况下就需要时间控制Petri网,以使转换与非零时间相联系。,2019

25、/6/4,湖南科技大学 计算机学院 戴祖雄,43,2. 楼层按钮 在Petri网中楼层按钮用位置 和 表示,分别代表f楼层请求电梯上行和下行的按钮。底层的按钮为 ,最高层的按钮为 ,中间每一层有两个按钮 和 (1fm)。 图4.11所示的情况为电梯由g层驶向f层。根据电梯乘客的要求,某一个楼层按钮亮或两个楼层按钮都亮。如果两个按钮都亮了,则只有一个按钮熄灭。图4.11所示的Petri网可以保证,当两个按钮都亮了的时候,只有一个按钮熄灭。但是要保证按钮熄灭正确,则需要更复杂的Petri网模型。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,44,图4.11 Petri网表示楼层按钮,201

26、9/6/4,湖南科技大学 计算机学院 戴祖雄,45,最后,让我们考虑第三条约束。 第三条约束C3：当电梯没有收到请求时,它将停留在当前楼层并关门。 这条约束很容易实现,如图 4.11所示,当没有请求( 和 上无令牌)时,任何一个转换“电梯在运行”都不能被激发。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,46,4.4 Z语言,4.4.1 简介 本节结合电梯问题的例子,简要地介绍Z语言。 用Z语言描述的、最简单的形式化规格说明含有下述4个部分: 给定的集合、数据类型及常数。 状态定义。 初始状态。 操作。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,47,1. 给定的集合 一个Z

27、规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合,这种集合用带方括号的形式表示。对于电梯问题,给定的初始化集合称为Button,即所有按钮的集合,因此,Z规格说明开始于： Button,2019/6/4,湖南科技大学 计算机学院 戴祖雄,48,2. 状态定义 一个Z规格说明由若干个“格(schema)”组成,每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如,格S的格式如图4.12所示。 在电梯问题中,Button有4个子集,即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮

28、的集合)以及pushed(所有被按的按钮的集合,即所有处于打开状态的按钮的集合)。图4.13描述了格Button_State,其中,符号P表示幂集(即给定集的所有子集)。约束条件声明,floor_buttons集与elevator_buttons集不相交,而且它们共同组成buttons集。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,49,图4.12 Z格S的格式,2019/6/4,湖南科技大学 计算机学院 戴祖雄,50,图4.13 Z格Button_State,2019/6/4,湖南科技大学 计算机学院 戴祖雄,51,3. 初始状态 抽象的初始状态是指系统第一次开启时的状态。对于电梯

29、问题来说,抽象的初始状态为： Button_InitButton_Statepushed= 上式表示,当系统首次开启时pushed集为空,即所有按钮都处于关闭状态。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,52,4. 操作 如果一个原来处于关闭状态的按钮被按下,则该按钮开启,这个按钮就被添加到pushed集中。图4.14定义了操作Push_Button(按按钮)。Z语言的语法规定: 当一个格被用在另一个格中时,要在它的前面加上三角形符号作为前缀,因此,格Push_Button的第一行最前面有一个三角形符号作为格Button_State的前缀。操作Push_Button有一个输入变量

30、“button?”。问号“?”表示输入变量,而感叹号“!”代表输出变量。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,53,操作的谓词部分,包含了一组调用操作的前置条件,以及操作完全结束后的后置条件。如果前置条件成立,则操作执行完成后可得到后置条件。但是,如果在前置条件不成立的情况下调用该操作,则不能得到指定的结果(因此结果无法预测)。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,54,图4.14中的第一个前置条件规定, “button?”必须是buttons的一个元素, 而buttons是电梯系统中所有按钮的集合。如果第二个前置条件button?pushed得到满足(即按钮没

31、有开启), 则更新pushed按钮集,使之包含刚开启的按钮“button?”。在Z语言中,当一个变量的值发生改变时,就用符号 表示。也就是说,后置条件是当执行完操作Push_Button之后,“button?”将被加入到pushed集中。我们无需直接打开按钮,只要使“button?”变成pushed中的一个元素即可。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,55,图4.14 操作Push_Button的Z规格说明,2019/6/4,湖南科技大学 计算机学院 戴祖雄,56,还有一种可能性是,被按的按钮原先已经打开了。由于button?pushed,根据第三个前置条件,将没有任何事情发

32、生,这可以用pushed=pushed来表示,即pushed的新状态和旧状态一样。注意,如果没有第三个前置条件,规格说明将不能说明在一个按钮已被按过之后又被按了一次的情况下将发生什么事,因此,结果将是不可预测的。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,57,假设电梯到达了某楼层,如果相应的楼层按钮已经打开,则此时它会关闭；同样,如果相应的电梯按钮已经打开,则此时它也会关闭。也就是说,如果“button?”属于pushed集,则将它移出该集合,如图4.15所示(符号“”表示集合差运算)。但是,如果按钮“button?”原先没有打开,则pushed集合不发生变化。,2019/6/4,

33、湖南科技大学 计算机学院 戴祖雄,58,图4.15 操作Floor_Arrival的Z规格说明,2019/6/4,湖南科技大学 计算机学院 戴祖雄,59,4.4.2 评价 Z语言之所以会获得如此多的成功,主要有以下几个原因: 可以比较容易地发现用Z写的规格说明的错误,特别是在自己审查规格说明,及根据形式化的规格说明来审查设计与代码时,情况更是如此。 用Z写规格说明时,要求作者十分精确地使用Z说明符。由于对精确性的要求很高,从而和非形式化规格说明相比,减少了模糊性、不一致性和遗漏。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,60,Z是一种形式化语言,在需要时开发者可以严格地验证规格说明

34、的正确性。 虽然完全学会Z语言相当困难,但是,经验表明,只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明,当然,这些人还没有能力证明规格说明的结果是否正确。 使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多,但开发过程所需要的总时间却减少了。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,61,虽然用户无法理解用Z写的规格说明,但是,可以依据Z规格说明用自然语言重写规格说明。经验证明,这样得到的自然语言规格说明,比直接用自然语言写出的非形式化规格说明更清楚、更正确。 使用形式化规格说明是全球的总趋势,过去,主要是欧洲习惯于使用形

35、式化规格说明技术,现在越来越多的美国公司也开始使用形式化规格说明技术。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,62,4.5 小结,基于数学的形式化规格说明技术,目前还没有在软件产业界广泛应用,但是,与欠形式化的方法比较起来,它确实有实质性的优点：形式化的规格说明可以用数学方法研究、验证(例如,一个正确的程序可以被证明满足其规格说明,两个规格说明可以被证明是等价的,规格说明中存在的某些形式的不完整性和不一致性可以被自动地检测出来)。此外,形式化的规格说明消除了二义性,而且它鼓励软件开发者在软件工程过程的早期阶段使用更严格的方法,从而可以减少差错。,2019/6/4,湖南科技大学 计

36、算机学院 戴祖雄,63,当然,形式化方法也有缺点：大多数形式化的规格说明主要关注于系统的功能和数据,而问题的时序、控制和行为等方面的需求却更难于表示。此外,形式化方法比欠形式化方法更难学习,不仅在培训阶段要花大量的投资,而且对某些软件工程师来说,它代表了一种“文化冲击”。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,64,把形式化方法和欠形式化方法有机地结合起来,使它们取长补短,应该能获得更理想的效果。本章讲述的应用形式化方法的准则(见4.1.3节),对于读者今后在实际工作中更好地利用形式化方法,可能是有帮助的。 本章简要地介绍了有穷状态机、Petri网和Z语言等三种典型的形式化方法,使读者对它们有初步的、概括的了解。当然,要想在实际工作中使用这些方法,还需要进一步研读有关的专著。,