程序设计方法学(六).ppt

《程序设计方法学(六).ppt》由会员上传分享，免费在线阅读，更多相关内容在PPT专区-天天文库。

1、第六章程序设计的形式化方法软件新技术智能化技术扩大软件功能的关键途径自动化技术提高软件生产率的根本途径集成化技术助于提高生产率、提高质量并行化技术提高系统实效的关键技术自然化技术实现社会信息化重要方向攻克的关键教技术网络体系传感器网与因特网的高效融合集成芯片从Systemonchip到Chipondemount虚拟计算资源聚合的有效性和可靠性验证软件工程基于网络环境的需求工程知识处理挖掘从消息到知识到决策的元知识高效系统在高性（效）能计算系统中系列关注信息安全信息教育跨越源之识规律创新根植辨短长汪成为院士软件自动化的三个层次软件自动化

2、（自动程序设计）广义：尽可能地借助计算机系统实现软件开发狭义：从形式化的软件功能规范到可执行程序代码这一过程的自动化从软件需求规范软件功能、性能规范的转换解决从“非形式”“形式”难度很大，寄希望于受限自然语言方面的突破从软件功能、性能规范软件设计从“做什么”“如何做“从软件设计规范高级语言已有相当的进展，出现了许多工具……§1概述一、重要意义软件发展中的问题：整体功能不强、缺乏智能、质量欠佳、生产效率低软件自动化是提高软件生产率的根本途径软件自动化的前提是形式化因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的

3、前提二、发展状况有30多年历史Dijkstra、Hoare――――程序验证Scott、Stratchey――――程序语义形式化方法(FormalMethod)：通过严格的规范化的数学理论来描述软件系统“做什么”的方法。需要形式规范语言的支持。形式规范语言：提供了一个称为语法域的记号系统。一个称为语义域的目标集合，以及一组精确定义的哪些目标系统满足那个规范的规则。因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。形式系统是二元组（L，Cn）L：语言（形式规范语言）Cn：对应关系，由推理规则构成在软件规范方法方面的

4、代表性成果有：⑴基于异调代数的代数方法特点：用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质，而不涉及数据的具体表示。基本理论：代数语义⑵抽象模型方法特点：基于某些已知的ADT来给出待定义的ADT的抽象模型，用抽象模型来刻画待定义的ADT中运算的功能。基本理论：指称语义⑶状态机方法特点：通过状态的转换来刻画输入与输出间的关系基本理论：操作语义⑷高阶软件方法（HOS）基于控制公理基本理论：公理语义在软件规范语言方面的代表性成果有：一阶谓词演算组成语言80年代：Z语言、Larch语言、VDM语言90年代：面向实时及分布式的LOTOS

5、语言、面向对象的Z++、Object-Z、VDM++等三、分类⑴基于模型的方法给出系统（程序）状态和状态变换与操作的显式的表示但亦是抽象的定义，不涉及并发的行为。如：Z、VDM⑵代数方法通过联系不同的操作间的行为关系给出操作的隐式定义，未给出并发的显式表示。如：OBJ、Larch⑶过程代数方法给出并发过程的一个显式模型，并通过过程间允许的可观察的通信上的限制来约束表示行为。如：CSP（通信顺序进程）和CCS（通信系统计算）⑷基于逻辑的方法采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间的行为规范。如：时态逻辑、模态逻辑⑸基于

6、网络的方法根据网络中的数据流显式地给出系统的并发模型，包括数据从一个结点流向另一个结点的条件。如：Petri网、谓词变换网四、形式化软件开发方法采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三方面模型：现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。开发过程中的任务为：模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。对应需求分析、设计等活动。模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。模型变换：是向计算机

7、系统变换的过程，关键的任务是一致性检测。对应实现和测试。三项任务分别对应三方面的活动：1.形式化规范（规格）：软件规范是指对软件系统对象及用来对系统对象进行操作的方法的集合。以及对所开发系统中的各对象在生命周期间的集体行为的描述。对应与软件生命周期的各个阶段，规范应该理解为是一个多阶段的行为。见例图规范可以采用非、半形式化的方法来描述，形式化规范精确地描述了用户的需求、软件系统的功能及各种性质，其描述的是“做什么”，而不考虑“如何做”。因此，在理解、掌握形式规范语言和方法的基础上对所描述的系统的全面、深入的了解，给出恰如其分的描述上至

8、关重要的。包含各规格阶段的生命周期模型例需求分析BSSRD系统设计1DS系统设计2PS软件开发代码实现软件测试运行SRD：软件需求文档BS：行为规范DS：设计规范PS：程序规范软件系统规范的形式化方法从形式化规范到目标软