软件工程形式化说明技术

软件工程形式化说明技术CreativepurehandpaintedbusinesspresentationsCreativepurehandpaintedbusinesspresentations汇报人：视觉设计部门：创意设计部浪费时间是一桩大罪过。---卢梭人生不可能一帆风顺，有成功，也有失败；有开心，也有失落。如果我们把生活中的这些起起落落看得太重，那么生活对于我们来说永远都不会坦然，永远都没有欢笑。人生应该有所追求，但暂时得不到并不会阻碍日常生活的幸福，因此，拥有一颗平常心，是人生必不可少的润滑液剂。回到最单纯的初心，在最空的地方安坐，让世界的吵闹去喧嚣它们自己吧！让湖光山色去清秀它们自己吧！让人群从远处走开或者自身边擦过吧！普通人只想到如何度过时间，有才能的人设法利用时间。---德国哲学家叔本华我们总会长大，会试着去成熟，会学着去放弃，去包容一些，即使过程艰难又漫长，但要相信，天总会亮。软件工程形式化说明技术软件工程形式化说明技术CreativepurehandpaintedbusinesspresentationsCreativepurehandpaintedbusinesspresentations汇报人：视觉设计部门：创意设计部浪费时间是一桩大罪过。---卢梭人生不可能一帆风顺，有成功，也有失败；有开心，也有失落。如果我们把生活中的这些起起落落看得太重，那么生活对于我们来说永远都不会坦然，永远都没有欢笑。人生应该有所追求，但暂时得不到并不会阻碍日常生活的幸福，因此，拥有一颗平常心，是人生必不可少的润滑液剂。回到最单纯的初心，在最空的地方安坐，让世界的吵闹去喧嚣它们自己吧！让湖光山色去清秀它们自己吧！让人群从远处走开或者自身边擦过吧！普通人只想到如何度过时间，有才能的人设法利用时间。---德国哲学家叔本华我们总会长大，会试着去成熟，会学着去放弃，去包容一些，即使过程艰难又漫长，但要相信，天总会亮。关于形式化方法形式化方法是有争议的。它们的支持者宣称：它们可以引发软件开发的革命。而批评者认为：这是困难和不可能的。同时，对于大多数人来说，对形式化方法是如此不熟悉，以至难于判断这些争论。2形式化的程序非形式化方法：自然语言描述半形式化方法（欠形式化方法）：数据流图、实体-联系图形式化方法：一种方法有坚实的数学基础3非形式化方法的缺点二义性：操作员名和口令可能存在矛盾：监控温度/往往距离很远含糊性：由雷达操作员使用的系统界面应该是用户友好的不完整性：传感器抽象层次混乱：系统的目的是跟踪仓库中的库存/当店员输入命令withdraw及参数，系统将回馈是否允许移去货物4形式化方法的优点简洁几乎可以没有二义性可以通过数学方法来发现矛盾和不完整性在不同软件工程活动之间平滑地过渡提供了高层确认的手段5有穷状态机有穷状态机：可以准确的描述一个系统6有穷状态机有穷状态机的组成部分（五元组）状态集输入集转换函数初始态终态集7有穷状态机谓词：全局状态的函数“猫是动物”一句中的“是动物”就是一个谓词，而“猫”是客体“3大于2”中“大于”是一个谓词转换规则：当前状态[菜单]+事件[所选择的项]=>下个状态当前状态[菜单]+事件[所选择的项]+谓词=>下个状态8有穷状态机电梯系统的描述9有穷状态机10有穷状态机便于书写，验证可以通过CASE工具将有穷状态机的规格说明直接转变为源代码开发一个规模比较大的系统时，三元组数量太多没有处理定时需求11Petri网Petri网：最初用于自动化处理方面，后来才用于计算机科学中位置：用圆圈表示转换：用短直线表示用于转换的输入函数：由位置指向转换的箭头表示用于转换的输出函数：由转换指向位置的箭头表示12Petri网权标（Token）及权标的表示带权标的Petri网：是否允许转换禁止线：带小圆圈的输入线表示带禁止线的Petri网13Petri网14Petri网15有穷状态机便于书写，验证可以通过CASE工具将有穷状态机的规格说明直接转变为源代码开发一个规模比较大的系统时，三元组数量太多没有处理定时需求11Petri网Petri网：最初用于自动化处理方面，后来才用于计算机科学中位置：用圆圈表示转换：用短直线表示用于转换的输入函数：由位置指向转换的箭头表示用于转换的输出函数：由转换指向位置的箭头表示12Petri网权标（Token）及权标的表示带权标的Petri网：是否允许转换禁止线：带小圆圈的输入线表示带禁止线的Petri网13Petri网14Petri网15Z语言Z语言包含的内容：给定的集合、数据类型及常数状态定义初始状态操作16Z语言给定的集合：用[]表示状态定义：格（schema）初始状态操作：？表示输入变量，！表示输出变量，′表示某个变量的值发生了改变，＼表示差运算17Z语言18Z语言19Z语言20Z语言块处理21Z语言22Z语言23Z语言24Z语言用Z语言书写的规格说明，比较容易发现错误减少了模糊性、不一致性和遗漏可以严格验证规格说明的正确性虽然完全掌握Z语言困难，但是学会编写还是比较容易的使用Z语言可以降低软件开发费用和总时间从Z语言的规格说明转换出自然语言的规格说明更为清晰25应用形式化方法的准则应该选用适当的表示方法应该形式化，但不要过分形式化应该估算成本应该有形式化方法顾问随时提供咨询不应该放弃传统的开发方法应该建立详尽的文档不应该放弃质量标准不应该盲目依赖形式化方法应该测试、测试再测试应该重用2