程序设计方法学(大纲).ppt
2023/11/16,华东师大计算机科学技术系,1,程序设计方法学Programming Methodology,华东师范大学计算机科学技术系杨宗源,2023/11/16,华东师大计算机科学技术系,2,前言,从方法论角度讨论、研究程序设计（软件研发）重点：程序设计的原理、原则与技术目的：提高软件生产率 研究程序的性质以及程序设计的理论和方法的学科。基本内容一般可以包括：,2023/11/16,华东师大计算机科学技术系,3,程序的性质与特征程序的功能描述程序的正确性验证程序的推导与综合程序的结构分析程序语义的描述程序设计的策略与技术程序研制工具、环境 涉及程序设计理论、规范、研发技术（方法）、支持环境与自动程序设计等。,2023/11/16,华东师大计算机科学技术系,4,授课内容,第一章 综述第二章 程序的基本结构2.1 Prime程序 2.2 复合程序 2.3 结构定理2.4 递归结构定理第三章 程序的数据结构3.1 类型与类型系统程序 3.2 程序设计语言中的数据类型 3.3 数据抽象与抽象数据类型（ADT）3.4 面向对象方法3.5 面向方面编程,2023/11/16,华东师大计算机科学技术系,5,第四章 程序的正确性证明4.1 程序规范与程序的正确性定义 4.2 部分正确性证明方法 4.3 完全正确性证明方法 4.4 最弱前置谓词（WP)第五章 程序的形式推导方法5.1 面向目标的程序设计方法 5.2 不变式推导方法 第六章 程序设计的形式化方法6.1 概述6.2 基于代数方法的规范语言OBJ6.3基于模型方法的规范语言VDM,2023/11/16,华东师大计算机科学技术系,6,第七章 并行程序设计方法7.1 基本概念 7.2 并行系统 7.3 并行程序设计语言 7.4 通讯顺序进程(CSP),2023/11/16,华东师大计算机科学技术系,7,基本要求,了解程序设计方法学的地位和重要性；掌握程序控制结构构成的基本原理、基本成份；明确数据类型、数据抽象、抽象数据类型对程序设计及程序设计语言的影响及重要性并掌握相关技术；掌握程序正确性证明的基本方法，具有构造程序规范的能力；理解形式化软件开发的基本原理和典型方法；理解并行程序设计基本概念,具有并行程序设计的初步能力.,2023/11/16,华东师大计算机科学技术系,8,参考书,程序设计方法学基础陈火旺 湖南科学技术出版社 程序设计方法学 仲萃豪 吉林大学出版社 程序设计方法学教程 张幸儿 南京大学出版社 现代软件工程周之英 科学出版社形式语义学基础与形式说明 屈延文 科学出版社 The Science of Programming Gries,D.Communicating Sequential Programming from Specification Carroll Morgan程序设计方法学 胡正国 国防工业出版社 对象技术导论 冯玉琳 科学出版社,2023/11/16,华东师大计算机科学技术系,9,第一章 综述,一、发展回顾四、五十年代机器指令、汇编指令、FORTRAN、LISP、ALGOL语言的相继出现，主要用于科学计算。成就：冯.诺依曼提出存储程序 图灵提出自动装置的计算模型图灵抽象机 奠定了现代计算机的理论基础。评价标准：指令条数少存储单元省执行速度快,2023/11/16,华东师大计算机科学技术系,10,六，七十年代高级语言相继出现，编译技术（语言处理程序）成熟，完善，Compiler、OS、DBMS 三大系统软件日趋成熟，解决问题的规模，复杂性大为增加。软件危机出现 缺乏宏观上研究程序设计方法的重要性的认识。“程序设计比人们一般想象的远为复杂得多，其复杂程度超出了人类本身的智力、能力范围。”成就：数据结构和算法理论程序设计=数据结构+算法（Kunth1971）,2023/11/16,华东师大计算机科学技术系,11,b)形式化方法运用推理、逻辑断言等对程序的正确性进行验证 Floyd断言法（1967）通过断言（谓词公式）证明框图程序的正确性 Hoare公理化法（1969）著名的Hoare逻辑 PSQ。通过定义一个逻辑系统（含有程序公理及推导规则）证明程序部分/完全正确性 E.D.Dijkstra(1976)最弱前置谓词WP(S,Q)SQ、谓词转换,2023/11/16,华东师大计算机科学技术系,12,Gries 综合了以谓词演算为基础的证明系统，提出了“程序设计科学”，将程序设计从经验、技术、技巧升华为科学。对并行程序 提出了时态逻辑、模态逻辑，刻画安全性、事件性、优先性、并发性等程序性质。,2023/11/16,华东师大计算机科学技术系,13,c)软件工程化方法软件开发模型1968年北大西洋公约组织(NATO)召开软件工程会议，首次提出用工程化方法解决软件危机。Dijkstra（1969）提出”Goto语句”有害论。引起了讨论，导致形成“结构程序设计”的概念、原则、方法。Pascal语言诞生（Wirth 1971）i)强调程序结构和风格的良好性ii)以良好静态结构，保证程序动态执行的正确性,2023/11/16,华东师大计算机科学技术系,14,Wirth（1971）提出小规模程序设计和大规模程序设计本质的不同，提出了“自顶向下、逐步细化”，“分而治之、面向功能、功能分解”的思想。Parnas（1971）提出“信息隐藏”，模块化。Modula-2(1979)、C（1972）、Ada（1979）Unix OS、SA、SD、JSP等等,2023/11/16,华东师大计算机科学技术系,15,八、九十年代编程不再是主流，构造系统的方法（即系统的结构、接口、集成）。网络、分布式共享信息，协同工作。方法论与工程化 a)结构化程序设计方法 80s进入全盛时期，比较完备，称为传统方法。关系数据库管理系统（RDBMS）、SQL语言趋于成熟。传统的软件工程方法：功能分解法、数据流方法 JSD、信息造型法（E-R模型）,2023/11/16,华东师大计算机科学技术系,16,面向对象程序设计方法（O-O方法）1)O-O是程序设计新的规范 从面向过程 面向对象 一系列概念（如：继承、多态、封装）C/C+、Eiffel、Java、C#（.NET）2)O-O是信息系统设计的方法论面向对象分析、设计（OOAD）Coad/Yourdon面向对象的软件工程(OOSE)，用例（UseCase)建模 对象建模技术（OMT）G.BOOCH方法,2023/11/16,华东师大计算机科学技术系,17,责任驱动设计（RDD）CRC卡（类责任合作）VMT（可视化建模技术）UML（统一建模语言 Unified Module Language)RUP（Rational Unified Process)MDA（模型驱动体系结构 Model Diven Architechture）UML、XML、CORBA、Java 3）O-O是正在兴起的新技术 支持各类应用、不同种类的开发，重要的突破：软件的复用（Reuse）、应用框架（Application FrameWork)、软件架构（Software Architecture）,2023/11/16,华东师大计算机科学技术系,18,c）面向方面程序设计（Aspect-Oriented Programming），简称AOP。是为解决OO方法中的问题而出现的。该技术被评为21世纪对经济和人类生活工作方式最有影响力十种技术之一。AOP的核心思想是将软件系统中的横切关注点和核心关注点分别模块化，各自处理，再通过编织器进行无缝的编织实现，以解决代码纠缠等问题，降低耦合度，提高可维护、可重用、可扩展性。目前支持AOP的语言有AspectJ、AspectC、AspectC+、AspectC#、AspectS、AspectR（Ruby）及SpringAOP、JBossAop等等。,2023/11/16,华东师大计算机科学技术系,19,d）工程化的其他方法 i.计算机辅助软件工程（CASE）Unix 工具箱、Ada的开发环境、程序综合器、软件工具ii.基于构件（Component)的软件工程（CBSE）COM/COM+、CORBA、EJB设计模式(Gamma)“其重要性可以与70年代从编程中分离数据结构和算法作为程序设计的规律性成果相媲美”。,2023/11/16,华东师大计算机科学技术系,20,净室软件工程（Clean Room SE）集成：建模技术、形式化方法（程序验证等）、统计质量控制等方法、技术。目的：生成极高质量的软件。软件过程CMM体系、CMMi轻载软件工程（Agile开发方法、敏捷软件开发方法）eXtreme Programming（极值编程）SCRUM开发方法FDD（特征驱动开发方法）DSDM（动态系统开发方法）,2023/11/16,华东师大计算机科学技术系,21,d)形式化的方法计算机语言的研究可以分为三部分：语法学（Syntax)：研究程序设计语言的形态结构语义学（Semantics)：研究程序设计语言和它所指的对象间的关系语用学（Pragmatics)：研究语言和它使用间的关系形式语义学四个研究领域、四种程序计算模型 图灵机模型 谓词演算模型 代数模型递归函数论模型四种语义学 指称语义学代数语义学 公理语义学 操作语义学,2023/11/16,华东师大计算机科学技术系,22,i)指称语义采用形式系统方法，用相应的数学对象对一个既定形式语言的语义进行注释的学科。其基本思想是使语言的每一成分对应于一个数学对象，该对象就称为该语言成分的指称，程序视为输入域到输出域的映射。即存在两个域 语法域：定义一个形式语言系统 数学域：已知语义的形式系统方法：用一个语义解释函数，以语义域中的对象值来解释语法域中定义的语言对象的语义。基础：论域理论、演算、不动点理论成果：VDM（The Vienna Development Method),2023/11/16,华东师大计算机科学技术系,23,代数语义用代数方法对形式语言系统进行语义注释的学科基本思想是把描述语义的逻辑体系和满足这个逻辑系统的各种模型统一在一起，并把模型的集合视为是一代数机构，研究这些模型间的关系。基础：ADT（抽象数据类型）、泛代数、范畴论方法：寻找合适的模型代数，定义一个抽象数据类型（ADT）的不同语义，采用代数方法论证规范的正确性和实现的正确性。成果：OBJ语言（代数形式化规范语言）,2023/11/16,华东师大计算机科学技术系,24,操作语义用机器模型语言来解释语言的语义，基本思想是建立一个抽象机器以模拟程序在执行过程中如何进行数据处理。如：属性文法 除定义“做什么”（What），主要定义“如何做”（How）iv)公理语义把程序设计语言视为一个数据对象,建立它的公理系统，从而使程序设计语言有了坚实的基础。,2023/11/16,华东师大计算机科学技术系,25,这四类方法都可以形成规范语言（Specification Language），形成软件的自动化或半自动化技术。由形成的软件规范（由规范语言描述）采用演绎综合程序转换归纳综合过程实现机器学习等不同途径实现：从形式规范到程序、从程序到程序的推导,2023/11/16,华东师大计算机科学技术系,26,二、展望,今后的发展？软件开发对象的变化 数据处理数据无关信息技术信息 与一个语境（context）相关联,2023/11/16,华东师大计算机科学技术系,27,知识 知识：与多个语境相关联 智慧 智慧：基于不同来源的已有知识来创造的一般性原理,2023/11/16,华东师大计算机科学技术系,28,第二章 程序的控制结构,2.1 Prime程序一框图程序的基本结点函数结点：一个入口，一个出口 与赋值语句相对应，改变了程序中变量的值。,2023/11/16,华东师大计算机科学技术系,29,控制结点（谓词）：一个入口，两个出口P是谓词，按P的值为T或F决定控制流程，不改变程序中变量的值,2023/11/16,华东师大计算机科学技术系,30,聚合结点：二个入口，一个出口不执行任何运算,2023/11/16,华东师大计算机科学技术系,31,在一定条件下，一个程序可由上述结点组合而成：程序 框图指令 结点控制流 有向结点网在框图中将结点名去掉，则该框图可视为一种结构。称为框图结构。例1：框图程序：,2023/11/16,华东师大计算机科学技术系,32,p,f1,q,f2,2023/11/16,华东师大计算机科学技术系,33,二、Proper程序,一个框图程序，若满足：i）一个入口，一个出口（多个出口可由聚合结点汇聚成一个）。如：ii）每个结点总有一条从入口到出口的路径通过它。称其为Proper程序。例1是Proper程序。例2：非Proper程序的例子：,2023/11/16,华东师大计算机科学技术系,34,2023/11/16,华东师大计算机科学技术系,35,定理：一个Proper程序，总可以归结成一个函 数结点。证：归结方式：找出二个（或二个以上的）结点最小的Proper程序用一个函数结点替代它直至只有一个结点为止。例3：,2023/11/16,华东师大计算机科学技术系,36,三、Prime程序,Prime程序（又称初等程序、基本程序）是Proper程序且其中不包括由二个以上结点组成的Proper子程序。即最小的Proper程序。例4：Prime程序有：非Prime程序有：,2023/11/16,华东师大计算机科学技术系,37,Prime程序：非Prime程序:,2023/11/16,华东师大计算机科学技术系,38,例5 Prime程序的几种重要形式：函数（func）序列（；）If-thenWhile-do,p,p,f,f,g,f,f,2023/11/16,华东师大计算机科学技术系,39,Repeat-untilIf-then-elseDo-while,p,q,f,f,g,f,g,2023/11/16,华东师大计算机科学技术系,40,2.2 复合程序,一、程序的等价Proper程序的执行图（E-chart）描述Proper程序所定义的执行路径。E-chart的构造法：（从Proper程序到E-chart）a）对聚合结点编号。b）以与Proper程序的入口线相连的结点为E-chart的根，并沿各路径至出口线。,2023/11/16,华东师大计算机科学技术系,41,c）对E-chart中每条路径，若当前路径的终止结点是未曾出现在该路径的结点，则把Proper程序中与此结点相连的所有出口线及其结点作为它的后继。d）执行路径终止在程序的出口或回溯路径中曾出现的结点。显然，过程终止（结点有限），得到是一棵有限树。,2023/11/16,华东师大计算机科学技术系,42,例6：例3中的框图程序是Proper程序，它的E-chart为：称 为repeat型结点，可以合并。Proper程序中无循环 chart图中无repeat型结点。程序的执行树（E-tree）是一棵树，描述了程序的所有可能的执行路径。构造方法：在E-chart中将所有的Repeat型结点用相应的子树替代，抹去所有聚合结点。,2023/11/16,华东师大计算机科学技术系,43,程序的等价 若两个程序有相同的E-tree，则称它们执行等价。若两个程序有相同的功能，则称它们功能等价。例7：程序与程序执行等价,p,f,f,f,p,2023/11/16,华东师大计算机科学技术系,44,再如：程序程序不是执行等价，但功能等价,g,p,q,g,q,p,2023/11/16,华东师大计算机科学技术系,45,结论：执行等价=功能等价，但功能等价执行等价。例8：do-while是Prime程序，但其执行等价的程序不是Prime程序,f,f,p,g,2023/11/16,华东师大计算机科学技术系,46,二、复合程序,一个Prime程序的函数结点用另一个Prime来替代，产生的一个Proper程序称为复合程序。例9：程序是由Prime程序if-then和repeat-until复合而成的。,p,f,q,2023/11/16,华东师大计算机科学技术系,47,复合程序：一组固定的Prime程序（称为基础系）经过有限次的替代运算而得到的Proper程序。将基础系P1，P2Pn所得到的复合程序全体记为P1，P2Pn。复合程序集的性质、大小由基础系决定。例10：由;,If-then得到的程序无循环。;，Repeat;，If-then，While;，If-then-else，While;，If-then-else，Repeat;，If-then与;，Repeat无法比较定义：由一组固定的基础系构成的复合程序，称为结构化程序。,2023/11/16,华东师大计算机科学技术系,48,2.3 结构定理,证明了程序的基本结构是三种prime程序。例：只用加法操作计算两个正整数的乘积，即：x0 y0 S z=x*yz:=0;u:=x;while u0 dobeginz:=z+y;u:=u-1;end,2023/11/16,华东师大计算机科学技术系,49,如还允许加倍、减半等操作，程序为：z:=0;u:=0;v:=0;while u0 do beginif odd(u)then z:=z+v;u:=u div 2;v:=v mul 2;end,2023/11/16,华东师大计算机科学技术系,50,结构定理：任何一个Proper程序功能等价于基础系;,if-then-else,while所复合的程序。证：考虑任意的Proper程序P，设P有n个结点（函数、谓词）i）对程序中的谓词、函数结点进行编号（1n）ii）引入一个计数器Liii）在编号的基础上为各输入/出线进行编号编号规则：对结点i：输入线编号为i，输出线为该结点后继结点的编号；出口线为0。,2023/11/16,华东师大计算机科学技术系,51,注：通过聚合结点至出口线的线编号为0。iv)对每个结点i构造新结点gi的方法是：,2023/11/16,华东师大计算机科学技术系,52,V）将P改造成测试L的程序F：,2023/11/16,华东师大计算机科学技术系,53,程序F：L1，while L0 do if L=1 then g1;else if L=2 then g2;else if L=n then gn;else I;F;,while,if-then-elseF与P等价。例11：,2023/11/16,华东师大计算机科学技术系,54,结构化定理的意义,任一复杂的控制结构可以用三种最基本的结构来表示。揭露了Proper程序的构造本质。可以从二方面来考察程序：函数结点 程序段写的过程（逐步细化）程序段 函数结点 读的过程（抽象）给出了如何将一个非结构化的程序转换为结构化程序的方法。,2023/11/16,华东师大计算机科学技术系,55,2.4 递归结构程序,问题：结构定理所给出的方法没有考虑程序的清晰性和有效性，有必要进行改进，可通过消除一些多余的计数器L的设置和测试。基本思想：对某些j0，若gj中不出现L:=j的赋值，可以用程序gj来替代所有出现在gi（ij）中的赋值L:=j。如此替代后，由于j不再赋值给L，可将L=j从if-then-else结构中去掉，则语句序列为g1，gj-1,gj+1 gn。这种替代可继续，直至出现如下情形终止。i）除L:=0外所有L赋值均被消除。ii）每个余下的gi中都含有L:=i的赋值,2023/11/16,华东师大计算机科学技术系,56,结论：当程序无循环时，程序中最后只出现L:=0，所以L可消除，当程序有循环时L不可消除。例12：对例11的改造 例13：,
