程序设计方学(六).pptVIP

第六章 程序设计的形式化方法 软件新技术 智能化技术 扩大软件功能的关键途径 自动化技术 提高软件生产率的根本途径 集成化技术 助于提高生产率、提高质量 并行化技术 提高系统实效的关键技术 自然化技术 实现社会信息化 重要方向 攻克的关键教技术 网络体系 传感器网与因特网的高效融合 集成芯片 从System on chip到Chip on demount 虚拟计算 资源聚合的有效性和可靠性验证 软件工程 基于网络环境的需求工程 知识处理 挖掘从消息到知识到决策的元知识 高效系统 在高性（效）能计算系统中系列关注 信息安全 信息教育 软件自动化的三个层次 软件自动化（自动程序设计） 广义：尽可能地借助计算机系统实现软件开发 狭义：从形式化的软件功能规范到可执行程序代码 这一过程的自动化 ? 从软件需求规范 ? 软件功能、性能规范的转换 解决从 “非形式” ? “形式” 难度很大，寄希望于受限自然语言方面的突破 从软件功能、性能规范 ? 软件设计 从“做什么” ? “如何做“ 从软件设计规范 ? 高级语言 已有相当的进展，出现了许多工具…… §1 概述 一、重要意义 软件发展中的问题： 整体功能不强、缺乏智能、质量欠佳、生产效率低 软件自动化是提高软件生产率的根本途径 软件自动化的前提是形式化 因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提 二、发展状况 有30多年历史 Dijkstra、Hoare ――――程序验证 Scott、Stratchey ――――程序语义 形式化方法(Formal Method)： 通过严格的规范化的数学理论来描述软件系统“做什么”的方法。需要形式规范语言的支持。 形式规范语言： 提供了一个称为语法域的记号系统。一个称为语义域的目标集合，以及一组精确定义的哪些目标系统满足那个规范的规则。???????? 因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。 形式系统是二元组（L，Cn） L：语言（形式规范语言） Cn：对应关系，由推理规则构成 在软件规范方法方面的代表性成果有： ⑴ 基于异调代数的代数方法 特点：用抽象代数中的公理化方法来刻画抽象数 据类型中运算的性质，而不涉及数据的具 体表示。 基本理论：代数语义 ⑵ 抽象模型方法 特点：基于某些已知的ADT来给出待定义的 ADT的抽象模型，用抽象模型来刻画待 定义的ADT中运算的功能。 基本理论：指称语义 ⑶ 状态机方法 特点：通过状态的转换来刻画输入与输出间的 关系 基本理论：操作语义 ⑷ 高阶软件方法（HOS） 基于控制公理 基本理论：公理语义 在软件规范语言方面的代表性成果有： 一阶谓词演算组成语言 80年代：Z语言、Larch语言、VDM语言 90年代：面向实时及分布式的LOTOS语言、 面向对象的Z++、Object-Z、VDM++等 三、分类 ⑴ 基于模型的方法 给出系统（程序）状态和状态变换与操作的显式的表示但亦是抽象的定义，不涉及并发的行为。 如：Z、VDM ⑵ 代数方法 通过联系不同的操作间的行为关系给出操作的隐式定义，未给出并发的显式表示。 如：OBJ、Larch ⑶ 过程代数方法 给出并发过程的一个显式模型，并通过过程间允许的可观察的通信上的限制来约束表示行为。 如：CSP（通信顺序进程）和CCS（通信系统计算） ⑷ 基于逻辑的方法 采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间的行为规范。 如：时态逻辑、模态逻辑 ⑸ 基于网络的方法 根据网络中的数据流显式地给出系统的并发模型，包括数据从一个结点流向另一个结点的条件。 如：Petri网、谓词变换网 四、形式化软件开发方法 采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三方面模型：现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。 开发过程中的任务为： 模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。对应需求分析、设计等活动。 模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。 模型变换：是向计算机系统变换的过程， 关键的任务是一致性检测。对应实现和测试。 三项任务分别