程序设计方法学Programming

1、程序设计方法学Programming Methodology选课介绍 华东师范大学计算机科学技术系杨宗源8/13/20221华东师大计算机科学技术系本课程是硕士研究生的学位基础课。要求学有余力、优秀的本科生可以选读。形式化方法是本课程的主要内容，如何使学生理解、掌握、运用该方法将贯穿于教学的始终。 从方法论角度讨论、研究程序设计（软件研发）重点：程序设计的原理、原则与技术目的：提高软件生产率 研究程序的性质以及程序设计的理论和方法的学科。基本内容一般可以包括：课程性质8/13/20222华东师大计算机科学技术系程序的性质与特征程序的功能描述程序的正确性验证程序的推导与综合程序的结构分析程序语义

2、的描述程序设计的策略与技术程序研制工具、 环境 涉及程序设计理论、规范、研发技术（方法）、支持环境与自动程序设计等。8/13/20223华东师大计算机科学技术系课程大纲第一章 综述第二章 程序的基本结构2.1 Prime程序 2.2 复合程序 2.3 结构定理2.4 递归结构定理第三章 程序的数据结构3.1 类型与类型系统程序 3.2 程序设计语言中的数据类型 3.3 数据抽象与抽象数据类型（ADT）3.4 面向对象方法3.5 面向方面编程8/13/20224华东师大计算机科学技术系第四章 程序的正确性证明4.1 程序规范与程序的正确性定义 4.2 部分正确性证明方法 4.3 完全正确性证明方

3、法 4.4 最弱前置谓词（WP) 第五章 程序的形式推导方法5.1 面向目标的程序设计方法 5.2 不变式推导方法 第六章 程序设计的形式化方法6.1 概述6.2 基于代数方法的规范语言OBJ6.3基于模型方法的规范语言VDM8/13/20225华东师大计算机科学技术系第七章 并行程序设计方法7.1 基本概念 7.2 并行系统 7.3 并行程序设计语言 7.4 通讯顺序进程(CSP) 8/13/20226华东师大计算机科学技术系基本要求 了解程序设计方法学的地位和重要性；掌握程序控制结构构成的基本原理、基本成份；明确数据类型、数据抽象、抽象数据类型对程序设计及程序设计语言的影响及重要性并掌握相

4、关技术；掌握程序正确性证明的基本方法，具有构造程序规范的能力；理解形式化软件开发的基本原理和典型方法；理解并行程序设计基本概念,具有并行程序设计的初步能力. 8/13/20227华东师大计算机科学技术系参考书 程序设计方法学基础陈火旺 湖南科学技术出版社 程序设计方法学 仲萃豪 吉林大学出版社 程序设计方法学教程 张幸儿 南京大学出版社 现代软件工程周之英 科学出版社形式语义学基础与形式说明 屈延文 科学出版社 The Science of Programming Gries, D. Communicating Sequential ProcessosHoare,C.A.RProgrammin

5、g from Specification Carroll Morgan程序设计方法学 胡正国 国防工业出版社 对象技术导论 冯玉琳 科学出版社 8/13/20228华东师大计算机科学技术系部分授课内容展示今后的发展？软件开发对象的变化 数据处理数据无关信息技术信息 与一个语境（context）相关联8/13/20229华东师大计算机科学技术系知识 知识： 与多个语境相关联 智慧 智慧： 基于不同来源的已有知识来创造的一般性原理8/13/202210华东师大计算机科学技术系结构定理：任何一个Proper程序功能等价于基础系;,if-then-else,while所复合的程序。证：。结构定理8/1

6、3/202211华东师大计算机科学技术系type String declare NULLString /*语法说明*/ ISNULL(String)Boolean LEN(String)Int ADDCHAR(String,Char)String CONCAT(String,String)String SUBSTR(String,Int,Int)String INDEX(String,String)Int for all s,tString, c,dChar, i,jInt let ISNULL(NULL)=true ISNULL(ADDCHAR(s,c)=false 8/13/202212华

7、东师大计算机科学技术系LEN(NULL)=0 LEN(ADDCHAR(s,c)=LEN(s)+1 CONCAT(s,NULL)=s CONCAT(s,ADDCHAR(t,d)= ADDCHAR(CONCAT(s,t),d) SUBSTR(NULL,i,j)=NULL SUBSTR(ADDCHAR(s,c),i,j)= if j=0 then NULL else if j=LEN(s)-i+2 then ADDCHAR(SUBSTR(s,I,j-1),c) else SUBSTR(s,i,j)8/13/202213华东师大计算机科学技术系INDEX(s,NULL)=LEN(s)+1 INDEX(

8、NULL,ADDCHAR(t,d)=0 INDEX(ADDCHAR(s,t),ADDCHAR(t,d)= if INDEX(s,ADDCHAR(t,d) 0 then INDEX(s,ADDCHAR(t,d) else if c=d and t=SUBSTR(s,LEN(s)-EN(t)+1,LEN(t)then LEN(s)-LEN(t)+1 else 0 end end String8/13/202214华东师大计算机科学技术系面向方面程序设计面向方面程序设计（Aspect-Oriented Programming），简称AOP，是一种新的程序设计技术，是对目前主流的程序设计技术面向对象技

9、术的重要的扩展。它将影响多个类的行为封装到一个可重用模块，即Aspect中，从而解决了传统程序设计方法所带来的代码混乱和分散问题，为进一步增强了代码的重用性和灵活性提供了可能的途径。8/13/202215华东师大计算机科学技术系Hoare关于程序正确性的定义 给定Spec(,)，若对输入x满足(x)，则程序S计算终止，且(x,z)满足。称S关于(,)是完全正确的。记为S 给定Spec(,)，若对输入x满足(x)，当程序S计算终止时，满足(x,z)。称S关于(,)是部分正确的。记为S8/13/202216华东师大计算机科学技术系最弱前置谓词（WP）一、定义与性质设是一个程序（语句），是一个后置谓

10、词定义最弱前置谓谓词（Weakest Pre-predicate） （，）为：满足从其中任一状态开始执行，必须在有限的时间内终止。且满足的所有状态的集合。 由的定义，显然有：（，） S 8/13/202217华东师大计算机科学技术系行向右对齐问题要求设计一个程序，在每一行的字间插入适当的空格，使得所有的行都在同一列结束，同时满足 a) 对不同的相邻字间的空格数至多差1b) 对偶数（奇数）行必须出现较多的空格在右 （左）端例如 justifyinglinesby insertingextrablanksis onetaskofatexteditor重排为： justifyinglinesby i

11、nsertingextrablanksis onetaskofatexteditor8/13/202218华东师大计算机科学技术系基于模型方法的规范语言VDMThe Vienna Development MethodVDM由IBM的Vienna实验室20世纪70年代提出的的一种形式化方法。最初是为了解决用形式化方法来开发编译系统，使语言的语法、语义的定义更为严格、更加系统化（如实现PL/1语言的语义规范）。当时用VDL用于语言的注释。得到广泛的应用VDM在欧洲得到发展，从70年代末到90年代在欧美许多研究机构和大学得到广泛的应用（如曼彻斯特大学讲其作为必修课），以后逐渐称为一般的软件开发方法。8/13/202219华东师大计算机科学技术系哲学家就餐问题PHIL=*during ith lifetimeTHINK; room!enter( ); fork(i)!pickup( );fork(i+1)mod 5)!pickup( ); EAT; fork(i)!putdown( ); fork(i+1)mod(5)!putdown(f);room!exit(f)FORK=*phil(i)?pickup( )phil(i)?putdown( )phil(i-1)mod