《程序设计方法学》课件.pptVIP

程序设计方法学Programming Methodology 前言 从方法论角度讨论、研究程序设计（软件研发） 重点：程序设计的原理、原则与技术 目的：提高软件生产率 研究程序的性质以及程序设计的理论和方法的学科。基本内容一般可以包括： 程序的性质与特征 程序的功能描述 程序的正确性验证 程序的推导与综合 程序的结构分析 程序语义的描述 程序设计的策略与技术 程序研制工具、 环境 涉及程序设计理论、规范、研发技术（方法）、支持环境与自动程序设计等。 授课内容 第一章 综述 第二章 程序的基本结构 §2.1 Prime程序 §2.2 复合程序 §2.3 结构定理 §2.4 递归结构定理 第三章 程序的数据结构 §3.1 类型与类型系统程序 §3.2 程序设计语言中的数据类型 §3.3 数据抽象与抽象数据类型（ADT） §3.4 面向对象方法 §3.5 面向方面编程 第四章 程序的正确性证明 §4.1 程序规范与程序的正确性定义 §4.2 部分正确性证明方法 §4.3 完全正确性证明方法 §4.4 最弱前置谓词（WP) 第五章 程序的形式推导方法 §5.1 面向目标的程序设计方法 §5.2 不变式推导方法 第六章 程序设计的形式化方法 §6.1 概述 §6.2 基于代数方法的规范语言——OBJ §6.3基于模型方法的规范语言——VDM 第七章 并行程序设计方法 §7.1 基本概念 §7.2 并行系统 §7.3 并行程序设计语言 §7.4 通讯顺序进程(CSP) 基本要求 了解程序设计方法学的地位和重要性； 掌握程序控制结构构成的基本原理、基本成份； 明确数据类型、数据抽象、抽象数据类型对程序设计及程序设计语言的影响及重要性并掌握相关技术； 掌握程序正确性证明的基本方法，具有构造程序规范的能力； 理解形式化软件开发的基本原理和典型方法； 理解并行程序设计基本概念,具有并行程序设计的初步能力. 参考书 《程序设计方法学基础》陈火旺 湖南科学技术出版社 《程序设计方法学》 仲萃豪 吉林大学出版社 《程序设计方法学教程》 张幸儿 南京大学出版社 《现代软件工程》周之英 科学出版社 《形式语义学基础与形式说明》 屈延文 科学出版社 《The Science of Programming》 Gries, D. 《Communicating Sequential Processos》Hoare,C.A.R 《Programming from Specification》 Carroll Morgan 《程序设计方法学》 胡正国 国防工业出版社 《对象技术导论》 冯玉琳 科学出版社 第一章 综述 一、发展回顾 四、五十年代 机器指令、汇编指令、FORTRAN、LISP、ALGOL语言的相继出现，主要用于科学计算。 成就：冯.诺依曼 提出存储程序 图灵提出自动装置的计算模型 图灵抽象机 奠定了现代计算机的理论基础。 评价标准： 指令条数少 存储单元省 执行速度快 六，七十年代 高级语言相继出现， 编译技术（语言处理程序）成熟，完善，Compiler、OS、DBMS 三大系统软件日趋成熟，解决问题的规模， 复杂性大为增加。 软件危机出现 缺乏宏观上研究程序设计方法的重要性的认识。“程序设计比人们一般想象的远为复杂得多，其复杂程度超出了人类本身的智力、能力范围。” 成就： 数据结构和算法理论 程序设计 = 数据结构 + 算法 （Kunth 1971） b) 形式化方法 运用推理、逻辑断言等对程序的正确性进行验证 Floyd断言法（1967） 通过断言（谓词公式）证明框图程序的正确性 Hoare公理化法（1969） 著名的Hoare逻辑 {P}S{Q}。 通过定义一个逻辑系统（含有程序公理及推导规则）证明程序部分/完全正确性 E.D.Dijkstra (1976) 最弱前置谓词{WP(S,Q)}S{Q}、谓词转换 Gries 综合了以谓词演算为基础的证明系统，提出了“程序设计科学”，将程序设计从经验、技术、技巧升华为科学。 对并行程序 提出了时态逻辑、模态逻辑，刻画安全性、事件性、优先性、并发性等程序性质。 c) 软件工程化方法——软件开发模型 1968年 北大西洋公约组织(NATO)召开软件工程会议，首次提出用工程化方法解决软件危机。 Dijkstra（1969） 提出”Goto语句”有害论。引起了讨论，导致形成“结构程序设计”的概念、原则、方法。 Pasca