程序設計方法學programming

1、2024/3/26,華東師大計算機科學技術系,1,本課程是碩士研究生的學位基礎課。要求學有余力、優(yōu)秀的本科生可以選讀。形式化方法是本課程的主要內(nèi)容，如何使學生理解、掌握、運用該方法將貫穿于教學的始終。 從方法論角度討論、研究程序設計（軟件研發(fā)）重點：程序設計的原理、原則與技術目的：提高軟件生產(chǎn)率 研究程序的性質(zhì)以及程序設計的理論和方法的學科。基本內(nèi)容一般可以包括：,課程性質(zhì),2024/3/26,華東師大計算機科學技術系,2,

2、程序的性質(zhì)與特征程序的功能描述程序的正確性驗證程序的推導與綜合程序的結(jié)構(gòu)分析程序語義的描述程序設計的策略與技術程序研制工具、 環(huán)境 涉及程序設計理論、規(guī)范、研發(fā)技術（方法）、支持環(huán)境與自動程序設計等。,2024/3/26,華東師大計算機科學技術系,3,課程大綱,第一章 綜述第二章 程序的基本結(jié)構(gòu)§2.1 Prime程序 §2.2 復合程序 §2.3 結(jié)構(gòu)定理§2.4

3、 遞歸結(jié)構(gòu)定理第三章 程序的數(shù)據(jù)結(jié)構(gòu)§3.1 類型與類型系統(tǒng)程序 §3.2 程序設計語言中的數(shù)據(jù)類型 §3.3 數(shù)據(jù)抽象與抽象數(shù)據(jù)類型（ADT）§3.4 面向?qū)ο蠓椒?#167;3.5 面向方面編程,2024/3/26,華東師大計算機科學技術系,4,第四章 程序的正確性證明§4.1 程序規(guī)范與程序的正確性定義 §4.2 部分正確性證明方法 §4

4、.3 完全正確性證明方法 §4.4 最弱前置謂詞（WP) 第五章 程序的形式推導方法§5.1 面向目標的程序設計方法 §5.2 不變式推導方法 第六章 程序設計的形式化方法§6.1 概述§6.2 基于代數(shù)方法的規(guī)范語言——OBJ§6.3基于模型方法的規(guī)范語言——VDM,2024/3/26,華東師大計算機科學技術系,5,第七章 并行程序設計方法&#

5、167;7.1 基本概念 §7.2 并行系統(tǒng) §7.3 并行程序設計語言 §7.4 通訊順序進程(CSP),2024/3/26,華東師大計算機科學技術系,6,基本要求,了解程序設計方法學的地位和重要性；掌握程序控制結(jié)構(gòu)構(gòu)成的基本原理、基本成份；明確數(shù)據(jù)類型、數(shù)據(jù)抽象、抽象數(shù)據(jù)類型對程序設計及程序設計語言的影響及重要性并掌握相關技術；掌握程序正確性證明的基本方法，具有構(gòu)造程序規(guī)范的能力

6、；理解形式化軟件開發(fā)的基本原理和典型方法；理解并行程序設計基本概念,具有并行程序設計的初步能力.,2024/3/26,華東師大計算機科學技術系,7,參考書,《程序設計方法學基礎》陳火旺 湖南科學技術出版社 《程序設計方法學》 仲萃豪 吉林大學出版社 《程序設計方法學教程》 張幸兒 南京大學出版社 《現(xiàn)代軟件工程》周之英 科學出版社《形式語義學基礎與形式說明》 屈延文 科學出版社 《The Science of

7、Programming》 Gries, D. 《Communicating Sequential Processos》Hoare,C.A.R《Programming from Specification》 Carroll Morgan《程序設計方法學》 胡正國 國防工業(yè)出版社 《對象技術導論》 馮玉琳 科學出版社,2024/3/26,華東師大計算機科學技術系,8,部分授課內(nèi)容展示,今后的發(fā)展？軟件開發(fā)對象的變化 數(shù)

8、據(jù)處理數(shù)據(jù)無關信息技術信息 與一個語境（context）相關聯(lián),,,,,,2024/3/26,華東師大計算機科學技術系,9,知識 知識： 與多個語境相關聯(lián) 智慧 智慧： 基于不同來源的已有知識來創(chuàng)造的一般性原理,,,2024/3/26,華東師大計算機科學技術系,10,結(jié)構(gòu)定理：任何一個Proper程序功能等價于基礎系{;,if-then

9、-else,while}所復合的程序。證：。。。。。。,,結(jié)構(gòu)定理,2024/3/26,華東師大計算機科學技術系,11,type String declare NULL?String /*語法說明*/ ISNULL(String)?Boolean LEN(String)?Int ADDCHAR(String,C

10、har)?String CONCAT(String,String)?String SUBSTR(String,Int,Int)?String INDEX(String,String)?Int for all s,t?String, c,d?Char, i,j?Int let ISNULL(NULL)=true

11、 ISNULL(ADDCHAR(s,c))=false,2024/3/26,華東師大計算機科學技術系,12,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

12、,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)

13、,2024/3/26,華東師大計算機科學技術系,13,INDEX(s,NULL)=LEN(s)+1 INDEX(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

14、,LEN(s)-EN(t)+1,LEN(t))then LEN(s)-LEN(t)+1 else 0 end end String,2024/3/26,華東師大計算機科學技術系,14,面向方面程序設計,面向方面程序設計（Aspect-Oriented Programming），簡稱AOP，是一種新的程序設計技術，是對目前主流的程序設計技術——面向?qū)ο蠹夹g的重

15、要的擴展。它將影響多個類的行為封裝到一個可重用模塊，即Aspect中，從而解決了傳統(tǒng)程序設計方法所帶來的代碼混亂和分散問題，為進一步增強了代碼的重用性和靈活性提供了可能的途徑。,2024/3/26,華東師大計算機科學技術系,15,Hoare關于程序正確性的定義,⑴ 給定Spec(φ,Ψ)，若對輸入x滿足φ(x)，則程序S計算終止，且Ψ(x,z)滿足。稱S關于(φ,Ψ)是完全正確的。記為{φ}S{Ψ}⑵ 給定Spec(φ,

16、Ψ)，若對輸入x滿足φ(x)，當程序S計算終止時，滿足Ψ(x,z)。稱S關于(φ,Ψ)是部分正確的。記為[φ]S[Ψ],2024/3/26,華東師大計算機科學技術系,16,最弱前置謂詞（WP）,一、定義與性質(zhì)設Ｓ是一個程序（語句），Ψ是一個后置謂詞定義最弱前置謂謂詞（Weakest Pre-predicate） ＷＰ（Ｓ，Ψ）為：　滿足Ｓ從其中任一狀態(tài)開始執(zhí)行，必須在有限的時間內(nèi)終止。且滿足Ψ的所有狀態(tài)的集合。 由Ｗ

17、Ｐ的定義，顯然有：├{ＷＰ（Ｓ，Ψ）} S {Ψ},2024/3/26,華東師大計算機科學技術系,17,行向右對齊問題,要求設計一個程序，在每一行的字間插入適當?shù)目崭?，使得所有的行都在同一列結(jié)束，同時滿足 a) 對不同的相鄰字間的空格數(shù)至多差1b) 對偶數(shù)（奇數(shù)）行必須出現(xiàn)較多的空格在右 （左）端例如 justifying?lines?by???????? inserting?extra?blank

18、s?is?? one?task?of?a?text?editor??重排為： justifying?????lines?????by inserting?extra??blanks??is one??task??of?a?text?editor,2024/3/26,華東師大計算機科學技術系,18,基于模型方法的規(guī)范語言VDMThe Vienna Development Method,VDM由IBM的Vienn

19、a實驗室20世紀70年代提出的的一種形式化方法。最初是為了解決用形式化方法來開發(fā)編譯系統(tǒng)，使語言的語法、語義的定義更為嚴格、更加系統(tǒng)化（如實現(xiàn)PL/1語言的語義規(guī)范）。當時用VDL用于語言的注釋。得到廣泛的應用VDM在歐洲得到發(fā)展，從70年代末到90年代在歐美許多研究機構(gòu)和大學得到廣泛的應用（如曼徹斯特大學講其作為必修課），以后逐漸稱為一般的軟件開發(fā)方法。,2024/3/26,華東師大計算機科學技術系,19,哲學家就餐問題,PHIL=

20、*[…during ith lifetime…?THINK; 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(

21、i)?pickup( )?phil(i)?putdown( )?phil((i-1)mod(5)?pickup( ))?phil(i-1)mod(5)?putdown( )]ROOM=occupancy:int;occupancy:=0;*[(i:0..4)phil(i)?enter( )?occupancy:=occupancy+1 ? (i:0..4)phil(i)?exit( )?occupancy:=occupanc