程序设计方法学六.ppt
《程序设计方法学六.ppt》由会员分享,可在线阅读,更多相关《程序设计方法学六.ppt(71页珍藏版)》请在优知文库上搜索。
1、4/2/20231第六章第六章 程序设计的形式化方法程序设计的形式化方法 软件新技术软件新技术 智能化技术智能化技术 扩大软件功能的关键途径扩大软件功能的关键途径 自动化技术自动化技术 提高软件生产率的根本途径提高软件生产率的根本途径 集成化技术集成化技术 助于提高生产率、提高质量助于提高生产率、提高质量 并行化技术并行化技术 提高系统实效的关键技术提高系统实效的关键技术 自然化技术自然化技术 实现社会信息化实现社会信息化4/2/20232重要方向重要方向 攻克的关键教技术攻克的关键教技术网络体系网络体系 传感器网与因特网的高效融合传感器网与因特网的高效融合集成芯片集成芯片 从从System
2、on chip到到Chip on demount虚拟计算虚拟计算 资源聚合的有效性和可靠性验证资源聚合的有效性和可靠性验证软件工程软件工程 基于网络环境的需求工程基于网络环境的需求工程知识处理知识处理 挖掘从消息到知识到决策的元知识挖掘从消息到知识到决策的元知识高效系统高效系统 在高性(效)能计算系统中系列关注在高性(效)能计算系统中系列关注 信息安全信息安全信息教育信息教育4/2/20233跨越源之识规律跨越源之识规律创新根植辨短长创新根植辨短长汪成为院士4/2/20234软件自动化的三个层次软件自动化的三个层次 软件自动化(自动程序设计)软件自动化(自动程序设计)广义:尽可能地借助计算机系
3、统实现软件开发广义:尽可能地借助计算机系统实现软件开发狭义:从形式化的软件功能规范到可执行程序代码狭义:从形式化的软件功能规范到可执行程序代码 这一过程的自动化这一过程的自动化 从软件需求规范从软件需求规范 软件功能、性能规范的转换软件功能、性能规范的转换解决从解决从 “非形式非形式” “形式形式”难度很大,寄希望于受限自然语言方面的突破难度很大,寄希望于受限自然语言方面的突破 从软件功能、性能规范从软件功能、性能规范 软件设计软件设计从从“做什么做什么” “如何做如何做“ 从软件设计规范从软件设计规范 高级语言高级语言 已有相当的进展,出现了许多工具已有相当的进展,出现了许多工具4/2/20
4、2351 概述概述一、重要意义一、重要意义 软件发展中的问题:软件发展中的问题: 整体功能不强、缺乏智能、质量欠佳、生产效整体功能不强、缺乏智能、质量欠佳、生产效率低率低 软件自动化是提高软件生产率的根本途径软件自动化是提高软件生产率的根本途径 软件自动化的前提是形式化软件自动化的前提是形式化 因此将形式化的理论和方法用于需求分析与规格因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提说明是实现软件自动化的前提4/2/20236二、发展状况二、发展状况 有有30多年历史多年历史Dijkstra、Hoare程序验证程序验证 Scott、Stratchey 程序语义程序语义 形式
5、化方法形式化方法(Formal Method):通过严格的规范化的数学理论来描述软件系统通过严格的规范化的数学理论来描述软件系统“做做什么什么”的方法。需要形式规范语言的支持。的方法。需要形式规范语言的支持。 形式规范语言:形式规范语言:提供了一个称为语法域的记号系统。一个称为语义提供了一个称为语法域的记号系统。一个称为语义域的目标集合,以及一组精确定义的哪些目标系统域的目标集合,以及一组精确定义的哪些目标系统满足那个规范的规则。满足那个规范的规则。 4/2/20237 因此,形式化方法是在软件系统的开发过程中使用因此,形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。一种形
6、式系统来表示模型的方法。 形式系统是二元组(形式系统是二元组(L,Cn) L:语言(形式规范语言):语言(形式规范语言) Cn:对应关系,由推理规则构成:对应关系,由推理规则构成 在软件规范方法方面的代表性成果有:在软件规范方法方面的代表性成果有: 基于异调代数的代数方法基于异调代数的代数方法 特点:用抽象代数中的公理化方法来刻画抽象数特点:用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质,而不涉及数据的具据类型中运算的性质,而不涉及数据的具体表示。体表示。 基本理论:代数语义基本理论:代数语义4/2/20238抽象模型方法抽象模型方法 特点:基于某些已知的特点:基于某些已知的ADT来给
7、出待定义的来给出待定义的 ADT的抽象模型,用抽象模型来刻画待的抽象模型,用抽象模型来刻画待 定义的定义的ADT中运算的功能。中运算的功能。 基本理论:指称语义基本理论:指称语义状态机方法状态机方法 特点:通过状态的转换来刻画输入与输出间的特点:通过状态的转换来刻画输入与输出间的 关系关系 基本理论:操作语义基本理论:操作语义高阶软件方法(高阶软件方法(HOS) 基于控制公理基于控制公理 基本理论:公理语义基本理论:公理语义 4/2/20239 在软件规范语言方面的代表性成果有:在软件规范语言方面的代表性成果有: 一阶谓词演算组成语言一阶谓词演算组成语言 80年代:年代:Z语言、语言、Larc
8、h语言、语言、VDM语言语言 90年代:面向实时及分布式的年代:面向实时及分布式的LOTOS语言、语言、 面向对象的面向对象的Z+、Object-Z、VDM+等等三、分类三、分类基于模型的方法基于模型的方法 给出系统(程序)状态和状态变换与操作的显式的给出系统(程序)状态和状态变换与操作的显式的表示但亦是抽象的定义,不涉及并发的行为。表示但亦是抽象的定义,不涉及并发的行为。 如:如:Z、VDM4/2/202310代数方法代数方法 通过联系不同的操作间的行为关系给出操作的隐通过联系不同的操作间的行为关系给出操作的隐式定义,未给出并发的显式表示。式定义,未给出并发的显式表示。 如:如:OBJ、La
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 程序设计 方法