搜索
1第4章形式化说明技术4.1概述4.2有穷状态机4.3Petri网4.4Z语言4.5小结2关于形式化方法形式化方法是有争议的。它们的支持者宣称：它们可以引发软件开发的革命。而批评者认为：这是困难和不可能的。同时，对于大多数人来说，对形式化方法是如此不熟悉，以至难于判断这些争论。3形式化的程序非形式化方法：自然语言描述半形式化方法（欠形式化方法）：数据流图、实体-联系图形式化方法：一种方法有坚实的数学基础4非形式化方法的缺点二义性：操作员名和口令可能存在矛盾：监控温度/往往距离很远含糊性：由雷达操作员使用的系统界面应该是用户友好的不完整性：传感器抽象层次混乱：系统的目的是跟踪仓库中的库存/当店员输入命令withdraw及参数，系统将回馈是否允许移去货物5形式化方法的优点简洁几乎可以没有二义性可以通过数学方法来发现矛盾和不完整性在不同软件工程活动之间平滑地过渡提供了高层确认的手段6有穷状态机有穷状态机：可以准确的描述一个系统7有穷状态机有穷状态机的组成部分（五元组）状态集输入集转换函数初始态终态集8有穷状态机谓词：全局状态的函数“猫是动物”一句中的“是动物”就是一个谓词，而“猫”是客体“3大于2”中“大于”是一个谓词转换规则：当前状态[菜单]+事件[所选择的项]=下个状态当前状态[菜单]+事件[所选择的项]+谓词=下个状态9有穷状态机电梯系统的描述10有穷状态机11有穷状态机便于书写，验证可以通过CASE工具将有穷状态机的规格说明直接转变为源代码开发一个规模比较大的系统时，三元组数量太多没有处理定时需求12Petri网Petri网：最初用于自动化处理方面，后来才用于计算机科学中位置：用圆圈表示转换：用短直线表示用于转换的输入函数：由位置指向转换的箭头表示用于转换的输出函数：由转换指向位置的箭头表示13Petri网权标（Token）及权标的表示带权标的Petri网：是否允许转换禁止线：带小圆圈的输入线表示带禁止线的Petri网14Petri网15Petri网16Z语言Z语言包含的内容：给定的集合、数据类型及常数状态定义初始状态操作17Z语言给定的集合：用[]表示状态定义：格（schema）初始状态操作：？表示输入变量，！表示输出变量，′表示某个变量的值发生了改变，＼表示差运算18Z语言19Z语言20Z语言21Z语言块处理22Z语言23Z语言24Z语言25Z语言用Z语言书写的规格说明，比较容易发现错误减少了模糊性、不一致性和遗漏可以严格验证规格说明的正确性虽然完全掌握Z语言困难，但是学会编写还是比较容易的使用Z语言可以降低软件开发费用和总时间从Z语言的规格说明转换出自然语言的规格说明更为清晰26应用形式化方法的准则应该选用适当的表示方法应该形式化，但不要过分形式化应该估算成本应该有形式化方法顾问随时提供咨询不应该放弃传统的开发方法应该建立详尽的文档不应该放弃质量标准不应该盲目依赖形式化方法应该测试、测试再测试应该重用27形式化方法的未来发展目前还没有在业界广泛应用形式化技术主要关注于功能和数据，而问题的时序、控制和行为等方面却更难于表达有些问题元素（界面）也最好用图形技术来刻画形式化技术学习起来相对困难很有可能成为新一代CASE工具的基础28本章小结非形式化方法的缺点形式化方法的优点有限状态机Petri网Z语言形式化方法的未来发展