程序设计方法学(大纲) 课件

程序设计方法学ProgrammingMethodology

华东师范大学计算机科学技术系杨宗源9/26/20231华东师大计算机科学技术系程序设计方法学ProgrammingMethodology前言从方法论角度讨论、研究程序设计（软件研发）重点：程序设计的原理、原则与技术目的：提高软件生产率

研究程序的性质以及程序设计的理论和方法的学科。基本内容一般可以包括：9/26/20232华东师大计算机科学技术系前言从方法论角度讨论、研究程序设计（软件研发）8/7/202程序的性质与特征程序的功能描述程序的正确性验证程序的推导与综合程序的结构分析程序语义的描述程序设计的策略与技术程序研制工具、

环境

涉及程序设计理论、规范、研发技术（方法）、支持环境与自动程序设计等。9/26/20233华东师大计算机科学技术系程序的性质与特征8/7/20233华东师大计算机科学技术系授课内容第一章综述第二章程序的基本结构§2.1Prime程序

§2.2复合程序

§2.3结构定理§2.4递归结构定理第三章程序的数据结构§3.1类型与类型系统程序§3.2程序设计语言中的数据类型§3.3数据抽象与抽象数据类型（ADT）§3.4面向对象方法§3.5面向方面编程9/26/20234华东师大计算机科学技术系授课内容第一章综述8/7/20234华东师大计算机科学技第四章程序的正确性证明§4.1程序规范与程序的正确性定义§4.2部分正确性证明方法§4.3完全正确性证明方法 §4.4最弱前置谓词（WP)

第五章程序的形式推导方法 §5.1面向目标的程序设计方法

§5.2不变式推导方法

第六章程序设计的形式化方法 §6.1概述 §6.2基于代数方法的规范语言——OBJ §6.3基于模型方法的规范语言——VDM9/26/20235华东师大计算机科学技术系第四章程序的正确性证明8/7/20235华东师大计算机科第七章并行程序设计方法 §7.1基本概念

§7.2并行系统

§7.3并行程序设计语言

§7.4通讯顺序进程(CSP)9/26/20236华东师大计算机科学技术系第七章并行程序设计方法8/7/20236华东师大计算机科学基本要求

了解程序设计方法学的地位和重要性；掌握程序控制结构构成的基本原理、基本成份；明确数据类型、数据抽象、抽象数据类型对程序设计及程序设计语言的影响及重要性并掌握相关技术；掌握程序正确性证明的基本方法，具有构造程序规范的能力；理解形式化软件开发的基本原理和典型方法；理解并行程序设计基本概念,具有并行程序设计的初步能力.9/26/20237华东师大计算机科学技术系基本要求了解程序设计方法学的地位和重要性；8/7/2023参考书

《程序设计方法学基础》陈火旺湖南科学技术出版社《程序设计方法学》仲萃豪吉林大学出版社《程序设计方法学教程》张幸儿南京大学出版社《现代软件工程》周之英科学出版社《形式语义学基础与形式说明》屈延文科学出版社《TheScienceofProgramming》Gries,D.《CommunicatingSequentialProcessos》Hoare,C.A.R《ProgrammingfromSpecification》CarrollMorgan《程序设计方法学》胡正国国防工业出版社《对象技术导论》冯玉琳科学出版社9/26/20238华东师大计算机科学技术系参考书《程序设计方法学基础》陈火旺湖南科学技术出版社第一章综述

一、发展回顾四、五十年代 机器指令、汇编指令、FORTRAN、LISP、ALGOL语言的相继出现，主要用于科学计算。 成就：冯.诺依曼 提出存储程序 图灵提出自动装置的计算模型 图灵抽象机 奠定了现代计算机的理论基础。 评价标准： 指令条数少 存储单元省 执行速度快9/26/20239华东师大计算机科学技术系第一章综述一、发展回顾8/7/20239华东师大计算机科六，七十年代 高级语言相继出现，编译技术（语言处理程序）成熟，完善，Compiler、OS、DBMS三大系统软件日趋成熟，解决问题的规模，复杂性大为增加。软件危机出现

缺乏宏观上研究程序设计方法的重要性的认识。“程序设计比人们一般想象的远为复杂得多，其复杂程度超出了人类本身的智力、能力范围。”

成就：

数据结构和算法理论

程序设计=数据结构+算法（Kunth 1971）9/26/202310华东师大计算机科学技术系六，七十年代 8/7/202310华东师大计算机科学技术系b)形式化方法运用推理、逻辑断言等对程序的正确性进行验证Floyd断言法（1967） 通过断言（谓词公式）证明框图程序的正确性Hoare公理化法（1969） 著名的Hoare逻辑{P}S{Q}。 通过定义一个逻辑系统（含有程序公理及推导规则）证明程序部分/完全正确性E.D.Dijkstra (1976)最弱前置谓词{WP(S,Q)}S{Q}、谓词转换

9/26/202311华东师大计算机科学技术系b)形式化方法8/7/202311华东师大计算机科学技术系Gries 综合了以谓词演算为基础的证明系统，提出了“程序设计科学”，将程序设计从经验、技术、技巧升华为科学。对并行程序

提出了时态逻辑、模态逻辑，刻画安全性、事件性、优先性、并发性等程序性质。9/26/202312华东师大计算机科学技术系Gries 8/7/202312华东师大计算机科学技c) 软件工程化方法——软件开发模型1968年 北大西洋公约组织(NATO)召开软件工程会议，首次提出用工程化方法解决软件危机。Dijkstra（1969）提出”Goto语句”有害论。引起了讨论，导致形成“结构程序设计”的概念、原则、方法。 Pascal语言诞生（Wirth1971） i)

强调程序结构和风格的良好性 ii)

以良好静态结构， 保证程序动态执行的正确性9/26/202313华东师大计算机科学技术系c) 软件工程化方法——软件开发模型8/7/202313华Wirth（1971） 提出小规模程序设计和大规模程序设计本质的不同，提出了“自顶向下、逐步细化”，“分而治之、面向功能、功能分解”的思想。Parnas（1971） 提出“信息隐藏”，模块化。Modula-2(1979)、C（1972）、Ada（1979）UnixOS、SA、SD、JSP等等9/26/202314华东师大计算机科学技术系Wirth（1971）8/7/202314华东师大计算机科学八、九十年代编程不再是主流，构造系统的方法（即系统的结构、接口、集成）。网络、分布式共享信息，协同工作。方法论与工程化a)

结构化程序设计方法 80’s进入全盛时期，比较完备，称为传统方法。关系数据库管理系统（RDBMS）、SQL语言趋于成熟。传统的软件工程方法： 功能分解法、数据流方法 JSD、信息造型法（E-R模型）

9/26/202315华东师大计算机科学技术系八、九十年代8/7/202315华东师大计算机科学技术系

面向对象程序设计方法（O-O方法） 1)

O-O是程序设计新的规范 从面向过程 面向对象 一系列概念（如：继承、多态、封装……） C/C++、Eiffel、Java、C#（.NET） 2)

O-O是信息系统设计的方法论 面向对象分析、设计（OOAD） Coad/Yourdon 面向对象的软件工程(OOSE)， 用例（UseCase)建模 对象建模技术（OMT） G.BOOCH方法9/26/202316华东师大计算机科学技术系

面向对象程序设计方法（O-O方法）8/7/20 责任驱动设计（RDD） CRC卡（类－责任－合作） VMT（可视化建模技术）UML（统一建模语言UnifiedModuleLanguage)RUP（RationalUnifiedProcess)MDA（模型驱动体系结构ModelDivenArchitechture） UML、XML、CORBA、Java3）O-O是正在兴起的新技术 支持各类应用、不同种类的开发，重要的突破：软件的复用（Reuse）、应用框架（ApplicationFrameWork)、软件架构（SoftwareArchitecture）

9/26/202317华东师大计算机科学技术系 责任驱动设计（RDD）8/7/202317华东师大计算机c）面向方面程序设计（Aspect-OrientedProgramming），简称AOP。是为解决OO方法中的问题而出现的。该技术被评为21世纪对经济和人类生活工作方式最有影响力十种技术之一。AOP的核心思想是将软件系统中的横切关注点和核心关注点分别模块化，各自处理，再通过编织器进行无缝的编织实现，以解决代码纠缠等问题，降低耦合度，提高可维护、可重用、可扩展性。目前支持AOP的语言有AspectJ、AspectC、AspectC++、AspectC#、AspectS、AspectR（Ruby）及SpringAOP、JBossAop等等。9/26/202318华东师大计算机科学技术系c）面向方面程序设计（Aspect-OrientedProd）工程化的其他方法i.

计算机辅助软件工程（CASE） Unix工具箱、Ada的开发环境、程序综合器、软件工具 ii.

基于构件（Component)的软件工程（CBSE）COM/COM+、CORBA、EJB 设计模式(Gamma)——“其重要性可以与70年代从编程中分离数据结构和算法作为程序设计的规律性成果相媲美”。 9/26/202319华东师大计算机科学技术系d）工程化的其他方法8/7/202319华东师大计算机

净室软件工程（CleanRoomSE） 集成：建模技术、形式化方法（程序验证等）、 统计质量控制等方法、技术。目的：生成极高质量的软件。软件过程 CMM体系、CMMi轻载软件工程 （Agile开发方法、敏捷软件开发方法） eXtremeProgramming（极值编程） SCRUM开发方法 FDD（特征驱动开发方法） DSDM（动态系统开发方法）9/26/202320华东师大计算机科学技术系净室软件工程（CleanRoomSE）8/7/2023d)

形式化的方法计算机语言的研究可以分为三部分：语法学（Syntax)：研究程序设计语言的形态结构语义学（Semantics)：研究程序设计语言和它所指的对象间的关系语用学（Pragmatics)：研究语言和它使用间的关系形式语义学四个研究领域、四种程序计算模型 图灵机模型

谓词演算模型

代数模型

递归函数论模型四种语义学指称语义学 代数语义学公理语义学 操作语义学9/26/202321华东师大计算机科学技术系d)

形式化的方法8/7/202321华东师大计算机科学i)

指称语义 采用形式系统方法，用相应的数学对象对一个既定形式语言的语义进行注释的学科。其基本思想是使语言的每一成分对应于一个数学对象，该对象就称为该语言成分的指称，程序视为输入域到输出域的映射。即存在两个域语法域：定义一个形式语言系统

数学域：已知语义的形式系统方法：用一个语义解释函数，

以语义域中的对象值来解释语法域中定义的语言对象的语义。基础：论域理论、λ演算、不动点理论成果：VDM（TheViennaDevelopmentMethod)9/26/202322华东师大计算机科学技术系i)

指称语义8/7/202322华东师大计算机科学技术系代数语义 用代数方法对形式语言系统进行语义注释的学科基本思想是把描述语义的逻辑体系和满足这个逻辑系统的各种模型统一在一起，并把模型的集合视为是一代数机构，研究这些模型间的关系。基础：ADT（抽象数据类型）、泛代数、范畴论方法：寻找合适的模型代数，

定义一个抽象数据类型（ADT）的不同语义，

采用代数方法论证规范的正确性和实现的正确性。成果：OBJ语言（代数形式化规范语言）9/26/202323华东师大计算机科学技术系代数语义8/7/202323华东师大计算机科学技术系操作语义 用机器模型语言来解释语言的语义，基本思想是建立一个抽象机器以模拟程序在执行过程中如何进行数据处理。 如：属性文法除定义“做什么”（What）， 主要定义“如何做”（How）iv)

公理语义 把程序设计语言视为一个数据对象, 建立它的公理系统，从而使程序设计语言有了坚实的基础。

9/26/202324华东师大计算机科学技术系操作语义8/7/202324华东师大计算机科学技术系这四类方法都可以形成规范语言（SpecificationLanguage），形成软件的自动化或半自动化技术。由形成的软件规范（由规范语言描述） 采用 演绎综合 程序转换 归纳综合 过程实现 机器学习等不同途径 实现：从形式规范到程序、从程序到程序的推导

9/26/202325华东师大计算机科学技术系这四类方法都可以形成规范语言（SpecificationL二、展望今后的发展？软件开发对象的变化

数据处理 数据 无关信息技术 信息 与一个语境（context）相关联9/26/202326华东师大计算机科学技术系二、展望今后的发展？8/7/202326华东师大计算机科学技知识

知识：

与多个语境相关联

智慧 智慧：基于不同来源的已有知识 来创造的一般性原理9/26/202327华东师大计算机科学技术系8/7/202327华东师大计算机科学技术系第二章程序的控制结构

§2.1Prime程序一．框图程序的基本结点函数结点：一个入口，一个出口

与赋值语句相对应，改变了程序中变量的值。9/26/202328华东师大计算机科学技术系第二章程序的控制结构§2.1Prime程序8/7/20控制结点（谓词）：一个入口，两个出口 P是谓词，按P的值为T或F决定控制流程，不改变程序中变量的值

9/26/202329华东师大计算机科学技术系控制结点（谓词）：一个入口，两个出口8/7/202329华东聚合结点：二个入口，一个出口

不执行任何运算

9/26/202330华东师大计算机科学技术系聚合结点：二个入口，一个出口8/7/202330华东师大计算在一定条件下，一个程序可由上述结点组合而成： 程序 框图 指令 结点 控制流

有向结点网在框图中将结点名去掉，则该框图可视为一种结构。称为框图结构。例1：框图程序：9/26/202331华东师大计算机科学技术系在一定条件下，一个程序可由上述结点组合而成：8/7/2023pf1qf29/26/202332华东师大计算机科学技术系pf1qf28/7/202332华东师大计算机科学技术系二、Proper程序

一个框图程序，若满足：i）一个入口，一个出口（多个出口可由聚合 结点汇聚成一个）。如：ii）每个结点总有一条从入口到出口的路径通 过它。称其为Proper程序。例1是Proper程序。例2：非Proper程序的例子：9/26/202333华东师大计算机科学技术系二、Proper程序一个框图程序，若满足：8/7/2029/26/202334华东师大计算机科学技术系8/7/202334华东师大计算机科学技术系定理：一个Proper程序，总可以归结成一个函 数结点。证：归结方式：找出二个（或二个以上的）结点最小的Proper程序用一个函数结点替代它直至只有一个结点为止。例3：……9/26/202335华东师大计算机科学技术系定理：一个Proper程序，总可以归结成一个函 数结三、Prime程序

Prime程序（又称初等程序、基本程序）

是Proper程序且其中不包括由二个以上结点组成的Proper子程序。即最小的Proper程序。例4：Prime程序有： 非Prime程序有：9/26/202336华东师大计算机科学技术系三、Prime程序Prime程序（又称初等程序、基本程序Prime程序： 非Prime程序:9/26/202337华东师大计算机科学技术系Prime程序： 非Prime程序:8/7/202例5Prime程序的几种重要形式：函数（func）序列（；）If-thenWhile-doppffgff9/26/202338华东师大计算机科学技术系例5Prime程序的几种重要形式：ppffgff8/7Repeat-untilIf-then-elseDo-whilepqf

fg

f

g9/26/202339华东师大计算机科学技术系pqffgfg8/7/202339华东师大计算机科§2.2复合程序

一、程序的等价Proper程序的执行图（E-chart）描述Proper程序所定义的执行路径。E-chart的构造法：（从Proper程序到E-chart）a）对聚合结点编号。b）以与Proper程序的入口线相连的结点为E-chart的根，并沿各路径至出口线。9/26/202340华东师大计算机科学技术系§2.2复合程序一、程序的等价8/7/202340华东c）对E-chart中每条路径，若当前路径的终止结点是未曾出现在该路径的结点，则把Proper程序中与此结点相连的所有出口线及其结点作为它的后继。d）执行路径终止在程序的出口或回溯路径中曾出现的结点。

显然，过程终止（结点有限），得到是一棵有限树。9/26/202341华东师大计算机科学技术系c）对E-chart中每条路径，若当前路径的终止结点是未曾出例6：例3中的框图程序是Proper程序，它的 E-chart为：……

称①②为repeat型结点，③④可以合并。Proper程序中无循环

chart图中无repeat型结点。程序的执行树（E-tree）

是一棵树，描述了程序的所有可能的执行路径。构造方法： 在E-chart中将所有的Repeat型结点用相应的子树替代，抹去所有聚合结点。

9/26/202342华东师大计算机科学技术系例6：例3中的框图程序是Proper程序，它的8/7/202程序的等价若两个程序有相同的E-tree，则称它们执行等价。若两个程序有相同的功能，则称它们功能等价。例7：程序与程序执行等价pfffp9/26/202343华东师大计算机科学技术系程序的等价pfffp8/7/202343华东师大计算机科学技再如：程序程序不是执行等价，但功能等价gpqgqp9/26/202344华东师大计算机科学技术系再如：程序gpqgqp8/7/20234结论：执行等价=>功能等价， 但功能等价≠>执行等价。例8：do-while是Prime程序，但其执行等价的程序不是Prime程序ffpg9/26/202345华东师大计算机科学技术系结论：执行等价=>功能等价，ffpg8/7/202二、复合程序一个Prime程序的函数结点用另一个Prime来替代，产生的一个Proper程序称为复合程序。例9：程序是由Prime程序if-then和repeat-until复合而成的。pfq9/26/202346华东师大计算机科学技术系二、复合程序一个Prime程序的函数结点用另一个Prime来复合程序：一组固定的Prime程序（称为基础系）经过有限次的替代运算而得到的Proper程序。将基础系P1，P2…Pn所得到的复合程序全体记为{P1，P2…Pn}。复合程序集的性质、大小由基础系决定。例10：由{;,If-then}得到的程序无循环。{;，Repeat}

{;，If-then，While}{;，If-then-else，While}≡{;，If-then-else，Repeat}{;，If-then}与{;，Repeat}无法比较定义：由一组固定的基础系构成的复合程序，称为结构化程序。

9/26/202347华东师大计算机科学技术系复合程序：一组固定的Prime程序（称为基础系）经过有限次的§2.3结构定理证明了程序的基本结构是三种prime程序。例：只用加法操作计算两个正整数的乘积，即： {x>0∧y>0}S{z=x*y} z:=0; u:=x; whileu≠0do begin z:=z+y; u:=u-1; end9/26/202348华东师大计算机科学技术系§2.3结构定理证明了程序的基本结构是三种prime程序如还允许加倍、减半等操作，程序为： z:=0;u:=0;v:=0; whileu≠0do begin ifodd(u)thenz:=z+v; u:=udiv2; v:=vmul2;end9/26/202349华东师大计算机科学技术系如还允许加倍、减半等操作，程序为：8/7/202349华东师结构定理：任何一个Proper程序功能等价于基础系{;,if-then-else,while}所复合的程序。证：考虑任意的Proper程序P，设P有n个结点（函数、谓词）i）对程序中的谓词、函数结点进行编号（1…n）ii）引入一个计数器Liii）在编号的基础上为各输入/出线进行编号编号规则：对结点i：输入线编号为i，输出线为该结点后继结点的编号；出口线为0。9/26/202350华东师大计算机科学技术系结构定理：任何一个Proper程序功能等价于基础系{;,if注：通过聚合结点至出口线的线编号为0。iv)对每个结点i构造新结点g