程序設(shè)計(jì)方法學(xué)programming

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

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

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

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

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

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

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

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

9、-else,while}所復(fù)合的程序。證：。。。。。。,,結(jié)構(gòu)定理,2024/3/26,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,11,type String declare NULL?String /*語(yǔ)法說(shuō)明*/ 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,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,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,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,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,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,14,面向方面程序設(shè)計(jì),面向方面程序設(shè)計(jì)（Aspect-Oriented Programming），簡(jiǎn)稱AOP，是一種新的程序設(shè)計(jì)技術(shù)，是對(duì)目前主流的程序設(shè)計(jì)技術(shù)——面向?qū)ο蠹夹g(shù)的重

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

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

17、Ｐ的定義，顯然有：├{ＷＰ（Ｓ，Ψ）} S {Ψ},2024/3/26,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,17,行向右對(duì)齊問(wèn)題,要求設(shè)計(jì)一個(gè)程序，在每一行的字間插入適當(dāng)?shù)目崭?，使得所有的行都在同一列結(jié)束，同時(shí)滿足 a) 對(duì)不同的相鄰字間的空格數(shù)至多差1b) 對(duì)偶數(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,華東師大計(jì)算機(jī)科學(xué)技術(shù)系,18,基于模型方法的規(guī)范語(yǔ)言VDMThe Vienna Development Method,VDM由IBM的Vienn

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