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

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

2、程序的性質(zhì)與特征程序的功能描述程序的正確性驗證程序的推導(dǎo)與綜合程序的結(jié)構(gòu)分析程序語義的描述程序設(shè)計的策略與技術(shù)程序研制工具、 環(huán)境 涉及程序設(shè)計理論、規(guī)范、研發(fā)技術(shù)（方法）、支持環(huán)境與自動程序設(shè)計等。,2024/3/26,華東師大計算機科學(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è)計語言中的數(shù)據(jù)類型 §3.3 數(shù)據(jù)抽象與抽象數(shù)據(jù)類型（ADT）§3.4 面向?qū)ο蠓椒?#167;3.5 面向方面編程,2024/3/26,華東師大計算機科學(xué)技術(shù)系,4,第四章 程序的正確性證明§4.1 程序規(guī)范與程序的正確性定義 §4.2 部分正確性證明方法 §4

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

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

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

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

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

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

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

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

17、Ｐ的定義，顯然有：├{ＷＰ（Ｓ，Ψ）} S {Ψ},2024/3/26,華東師大計算機科學(xué)技術(shù)系,17,行向右對齊問題,要求設(shè)計一個程序，在每一行的字間插入適當(dāng)?shù)目崭瘢沟盟械男卸荚谕涣薪Y(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,華東師大計算機科學(xué)技術(shù)系,18,基于模型方法的規(guī)范語言VDMThe Vienna Development Method,VDM由IBM的Vienn

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