1、程序設計方法學課件2022/10/7華東師大計算機科學技術系2前言從方法論角度討論、研究程序設計（軟件研發(fā)）重點：程序設計的原理、原則與技術目的：提高軟件生產率 研究程序的性質以及程序設計的理論和方法的學科?；緝热菀话憧梢园ǎ?022/10/7華東師大計算機科學技術系3程序的性質與特征程序的功能描述程序的正確性驗證程序的推導與綜合程序的結構分析程序語義的描述程序設計的策略與技術程序研制工具、 環(huán)境 涉及程序設計理論、規(guī)范、研發(fā)技術（方法）、支持環(huán)境與自動程序設計等。2022/10/7華東師大計算機科學技術系4授課內容第一章 綜述第二章 程序的基本結構2.1 Prime程序 2.2 復合程序

2、 2.3 結構定理2.4 遞歸結構定理第三章 程序的數(shù)據(jù)結構3.1 類型與類型系統(tǒng)程序 3.2 程序設計語言中的數(shù)據(jù)類型 3.3 數(shù)據(jù)抽象與抽象數(shù)據(jù)類型（ADT）3.4 面向對象方法3.5 面向方面編程2022/10/7華東師大計算機科學技術系5第四章 程序的正確性證明4.1 程序規(guī)范與程序的正確性定義 4.2 部分正確性證明方法 4.3 完全正確性證明方法 4.4 最弱前置謂詞（WP) 第五章 程序的形式推導方法5.1 面向目標的程序設計方法 5.2 不變式推導方法 第六章 程序設計的形式化方法6.1 概述6.2 基于代數(shù)方法的規(guī)范語言OBJ6.3基于模型方法的規(guī)范語言VDM2022/10/

3、7華東師大計算機科學技術系6第七章 并行程序設計方法7.1 基本概念 7.2 并行系統(tǒng) 7.3 并行程序設計語言 7.4 通訊順序進程(CSP) 2022/10/7華東師大計算機科學技術系7基本要求 了解程序設計方法學的地位和重要性；掌握程序控制結構構成的基本原理、基本成份；明確數(shù)據(jù)類型、數(shù)據(jù)抽象、抽象數(shù)據(jù)類型對程序設計及程序設計語言的影響及重要性并掌握相關技術；掌握程序正確性證明的基本方法，具有構造程序規(guī)范的能力；理解形式化軟件開發(fā)的基本原理和典型方法；理解并行程序設計基本概念,具有并行程序設計的初步能力. 2022/10/7華東師大計算機科學技術系8參考書 程序設計方法學基礎陳火旺 湖南科

4、學技術出版社 程序設計方法學 仲萃豪 吉林大學出版社 程序設計方法學教程 張幸兒 南京大學出版社 現(xiàn)代軟件工程周之英 科學出版社形式語義學基礎與形式說明 屈延文 科學出版社 The Science of Programming Gries, D. Programming from Specification Carroll Morgan程序設計方法學 胡正國 國防工業(yè)出版社 對象技術導論 馮玉琳 科學出版社 2022/10/7華東師大計算機科學技術系9第一章 綜述 一、發(fā)展回顧四、五十年代機器指令、匯編指令、FORTRAN、LISP、ALGOL語言的相繼出現(xiàn)，主要用于科學計算。成就：馮.諾依曼

5、提出存儲程序 圖靈提出自動裝置的計算模型圖靈抽象機 奠定了現(xiàn)代計算機的理論基礎。評價標準：指令條數(shù)少存儲單元省執(zhí)行速度快2022/10/7華東師大計算機科學技術系10六，七十年代高級語言相繼出現(xiàn)， 編譯技術（語言處理程序）成熟，完善，Compiler、OS、DBMS 三大系統(tǒng)軟件日趨成熟，解決問題的規(guī)模， 復雜性大為增加。軟件危機出現(xiàn) 缺乏宏觀上研究程序設計方法的重要性的認識?！俺绦蛟O計比人們一般想象的遠為復雜得多，其復雜程度超出了人類本身的智力、能力范圍?！?成就：數(shù)據(jù)結構和算法理論程序設計 = 數(shù)據(jù)結構 + 算法 （Kunth1971）2022/10/7華東師大計算機科學技術系11b) 形

6、式化方法運用推理、邏輯斷言等對程序的正確性進行驗證 Floyd斷言法（1967） 通過斷言（謂詞公式）證明框圖程序的正確性 Hoare公理化法（1969） 著名的Hoare邏輯 PSQ。通過定義一個邏輯系統(tǒng)（含有程序公理及推導規(guī)則）證明程序部分/完全正確性 E.D.Dijkstra(1976) 最弱前置謂詞WP(S,Q)SQ、謂詞轉換 2022/10/7華東師大計算機科學技術系12 Gries 綜合了以謂詞演算為基礎的證明系統(tǒng)，提出了“程序設計科學”，將程序設計從經驗、技術、技巧升華為科學。 對并行程序 提出了時態(tài)邏輯、模態(tài)邏輯，刻畫安全性、事件性、優(yōu)先性、并發(fā)性等程序性質。2022/10/7

7、華東師大計算機科學技術系13c)軟件工程化方法軟件開發(fā)模型1968年北大西洋公約組織(NATO)召開軟件工程會議，首次提出用工程化方法解決軟件危機。Dijkstra（1969）提出”Goto語句”有害論。引起了討論，導致形成“結構程序設計”的概念、原則、方法。Pascal語言誕生（Wirth 1971）i)強調程序結構和風格的良好性ii)以良好靜態(tài)結構， 保證程序動態(tài)執(zhí)行的正確性2022/10/7華東師大計算機科學技術系14Wirth（1971）提出小規(guī)模程序設計和大規(guī)模程序設計本質的不同，提出了“自頂向下、逐步細化”，“分而治之、面向功能、功能分解”的思想。Parnas（1971）提出“信息

8、隱藏”，模塊化。Modula-2(1979)、C（1972）、Ada（1979）Unix OS、SA、SD、JSP等等2022/10/7華東師大計算機科學技術系15八、 九十年代編程不再是主流，構造系統(tǒng)的方法 （即系統(tǒng)的結構、接口、集成）。網(wǎng)絡、分布式共享信息，協(xié)同工作。方法論與工程化 a) 結構化程序設計方法 80s進入全盛時期，比較完備，稱為傳統(tǒng)方法。關系數(shù)據(jù)庫管理系統(tǒng)（RDBMS）、SQL語言趨于成熟。傳統(tǒng)的軟件工程方法： 功能分解法、數(shù)據(jù)流方法 JSD、信息造型法（E-R模型） 2022/10/7華東師大計算機科學技術系16 面向對象程序設計方法（ O-O方法 ）1) O-O是程序設計

9、新的規(guī)范 從面向過程 面向對象 一系列概念（如：繼承、多態(tài)、封裝） C/C+、Eiffel、Java、C#（.NET）2) O-O是信息系統(tǒng)設計的方法論面向對象分析、設計（OOAD）Coad/Yourdon面向對象的軟件工程 (OOSE)，用例（UseCase)建模 對象建模技術（OMT）G.BOOCH方法2022/10/7華東師大計算機科學技術系17責任驅動設計（RDD）CRC卡（類責任合作）VMT（可視化建模技術） UML（統(tǒng)一建模語言 Unified Module Language) RUP（Rational Unified Process) MDA（模型驅動體系結構 Model Div

10、en Architechture）UML、XML、CORBA、Java 3）O-O是正在興起的新技術 支持各類應用、不同種類的開發(fā)，重要的突破：軟件的復用（Reuse）、應用框架（Application FrameWork)、軟件架構（Software Architecture） 2022/10/7華東師大計算機科學技術系18c）面向方面程序設計（Aspect-Oriented Programming），簡稱AOP。是為解決OO方法中的問題而出現(xiàn)的。該技術被評為21世紀對經濟和人類生活工作方式最有影響力十種技術之一。AOP的核心思想是將軟件系統(tǒng)中的橫切關注點和核心關注點分別模塊化，各自處理，再

11、通過編織器進行無縫的編織實現(xiàn)，以解決代碼糾纏等問題，降低耦合度，提高可維護、可重用、可擴展性。目前支持AOP的語言有AspectJ、 AspectC、 AspectC+、 AspectC#、 AspectS、 AspectR（Ruby）及SpringAOP、JBossAop等等。2022/10/7華東師大計算機科學技術系19 d）工程化的其他方法 i.計算機輔助軟件工程（CASE）Unix 工具箱、Ada的開發(fā)環(huán)境、程序綜合器、 軟件工具ii. 基于構件（Component)的軟件工程（CBSE） COM/COM+、CORBA、EJB設計模式(Gamma) “其重要性可以與70年代從編程中分離

12、數(shù)據(jù)結構和算法作為程序設計的規(guī)律性成果相媲美”。2022/10/7華東師大計算機科學技術系20 凈室軟件工程（Clean Room SE）集成：建模技術、形式化方法（程序驗證等）、 統(tǒng)計質量控制等方法、技術。 目的：生成極高質量的軟件。軟件過程CMM體系、CMMi輕載軟件工程（Agile開發(fā)方法、敏捷軟件開發(fā)方法）eXtreme Programming（極值編程）SCRUM開發(fā)方法FDD（特征驅動開發(fā)方法）DSDM （動態(tài)系統(tǒng)開發(fā)方法）2022/10/7華東師大計算機科學技術系21d) 形式化的方法計算機語言的研究可以分為三部分：語法學（Syntax)：研究程序設計語言的形態(tài)結構語義學（Sem

13、antics)：研究程序設計語言和它所指的對象間的關系語用學（Pragmatics)：研究語言和它使用間的關系形式語義學四個研究領域、四種程序計算模型 圖靈機模型 謂詞演算模型 代數(shù)模型遞歸函數(shù)論模型四種語義學 指稱語義學代數(shù)語義學 公理語義學 操作語義學2022/10/7華東師大計算機科學技術系22i)指稱語義采用形式系統(tǒng)方法，用相應的數(shù)學對象對一個既定形式語言的語義進行注釋的學科。其基本思想是使語言的每一成分對應于一個數(shù)學對象，該對象就稱為該語言成分的指稱，程序視為輸入域到輸出域的映射。即存在兩個域 語法域：定義一個形式語言系統(tǒng) 數(shù)學域：已知語義的形式系統(tǒng)方法：用一個語義解釋函數(shù)， 以語義

14、域中的對象值來解釋語法域中定義的語言對象的語義?；A：論域理論、演算、不動點理論成果：VDM（The Vienna Development Method)2022/10/7華東師大計算機科學技術系23代數(shù)語義用代數(shù)方法對形式語言系統(tǒng)進行語義注釋的學科基本思想是把描述語義的邏輯體系和滿足這個邏輯系統(tǒng)的各種模型統(tǒng)一在一起，并把模型的集合視為是一代數(shù)機構，研究這些模型間的關系?；A：ADT（抽象數(shù)據(jù)類型）、泛代數(shù)、范疇論方法：尋找合適的模型代數(shù)， 定義一個抽象數(shù)據(jù)類型（ADT）的不同語義， 采用代數(shù)方法論證規(guī)范的正確性和實現(xiàn)的正確性 。成果：OBJ語言（代數(shù)形式化規(guī)范語言）2022/10/7華東師大

15、計算機科學技術系24操作語義用機器模型語言來解釋語言的語義，基本思想是建立一個抽象機器以模擬程序在執(zhí)行過程中如何進行數(shù)據(jù)處理。如：屬性文法 除定義“做什么”（What），主要定義“如何做”（How）iv)公理語義把程序設計語言視為一個數(shù)據(jù)對象,建立它的公理系統(tǒng) ，從而使程序設計語言有了堅實的基礎。2022/10/7華東師大計算機科學技術系25這四類方法都可以形成規(guī)范語言（Specification Language），形成軟件的自動化或半自動化技術。 由形成的軟件規(guī)范（由規(guī)范語言描述）采用演繹綜合程序轉換歸納綜合過程實現(xiàn)機器學習等不同途徑實現(xiàn)：從形式規(guī)范到程序、從程序到程序的推導 2022/1

16、0/7華東師大計算機科學技術系26二、展望今后的發(fā)展？軟件開發(fā)對象的變化 數(shù)據(jù)處理數(shù)據(jù)無關信息技術信息 與一個語境（context）相關聯(lián)2022/10/7華東師大計算機科學技術系27知識 知識： 與多個語境相關聯(lián) 智慧 智慧： 基于不同來源的已有知識來創(chuàng)造的一般性原理2022/10/7華東師大計算機科學技術系28第二章 程序的控制結構 2.1 Prime程序一框圖程序的基本結點函數(shù)結點：一個入口，一個出口 與賦值語句相對應，改變了程序中變量的值。2022/10/7華東師大計算機科學技術系29控制結點（謂詞）：一個入口，兩個出口P是謂詞，按P的值為T或F決定控制流程，不改變程序中變量的值 20

17、22/10/7華東師大計算機科學技術系30聚合結點：二個入口，一個出口不執(zhí)行任何運算 2022/10/7華東師大計算機科學技術系31在一定條件下，一個程序可由上述結點組合而成：程序 框圖指令 結點控制流 有向結點網(wǎng)在框圖中將結點名去掉，則該框圖可視為一種結構。稱為框圖結構。例1：框圖程序： 2022/10/7華東師大計算機科學技術系32p f1q f22022/10/7華東師大計算機科學技術系33二、 Proper程序 一個框圖程序，若滿足： i）一個入口，一個出口（多個出口可由聚合結點匯聚成一個）。如： ii）每個結點總有一條從入口到出口的路徑通過它。 稱其為Proper程序。例1是Prop

18、er程序。例2：非Proper程序的例子：2022/10/7華東師大計算機科學技術系342022/10/7華東師大計算機科學技術系35定理：一個Proper程序，總可以歸結成一個函 數(shù)結點。 證：歸結方式：找出二個（或二個以上的）結點最小的Proper程序用一個函數(shù)結點替代它直至只有一個結點為止。例3：2022/10/7華東師大計算機科學技術系36三、Prime程序 Prime程序（ 又稱初等程序、基本程序）是Proper程序且其中不包括由二個以上結點組成的Proper子程序。 即最小的Proper程序。 例4：Prime程序有： 非Prime程序有：2022/10/7華東師大計算機科學技術系

19、37Prime程序： 非Prime程序:2022/10/7華東師大計算機科學技術系38例5 Prime程序的幾種重要形式：函數(shù)（func）序列（； ）If-thenWhile-doppf fgf f2022/10/7華東師大計算機科學技術系39Repeat-untilIf-then-elseDo-whilepqf f g f g2022/10/7華東師大計算機科學技術系402.2 復合程序 一、程序的等價Proper程序的執(zhí)行圖（E-chart） 描述Proper程序所定義的執(zhí)行路徑。E-chart的構造法： （從Proper程序到E-chart）a）對聚合結點編號。b）以與Proper程序的

20、入口線相連的結點為E-chart的根，并沿各路徑至出口線。2022/10/7華東師大計算機科學技術系41c）對E-chart中每條路徑，若當前路徑的終止結點是未曾出現(xiàn)在該路徑的結點，則把Proper程序中與此結點相連的所有出口線及其結點作為它的后繼。d）執(zhí)行路徑終止在程序的出口或回溯路徑中曾出現(xiàn)的結點。 顯然，過程終止（結點有限），得到是一棵有限樹。2022/10/7華東師大計算機科學技術系42例6：例3中的框圖程序是Proper程序，它的E-chart為： 稱 為repeat型結點，可以合并。Proper程序中無循環(huán) chart圖中無repeat型結點。程序的執(zhí)行樹（E-tree） 是一棵樹

21、，描述了程序的所有可能的執(zhí)行路徑。構造方法：在E-chart中將所有的Repeat型結點用相應的子樹替代，抹去所有聚合結點。 2022/10/7華東師大計算機科學技術系43程序的等價 若兩個程序有相同的E-tree，則稱它們執(zhí)行等價。 若兩個程序有相同的功能，則稱它們功能等價。 例7 ：程序與程序執(zhí)行等價pfffp2022/10/7華東師大計算機科學技術系44再如：程序程序不是執(zhí)行等價，但功能等價 g p q g q p2022/10/7華東師大計算機科學技術系45結論： 執(zhí)行等價=功能等價，但功能等價執(zhí)行等價。例8：do-while是Prime程序，但其執(zhí)行等價的程序不是Prime程序ffp

22、g2022/10/7華東師大計算機科學技術系46二、復合程序一個Prime程序的函數(shù)結點用另一個Prime來替代，產生的一個Proper程序稱為復合程序。例9：程序是由Prime程序if-then和repeat-until復合而成的。pf q2022/10/7華東師大計算機科學技術系47復合程序：一組固定的Prime程序（稱為基礎系）經過有限次的替代運算而得到的Proper程序。將基礎系P1，P2Pn所得到的復合程序全體記為P1，P2Pn。復合程序集的性質、大小由基礎系決定。例10：由;,If-then得到的程序無循環(huán)。;，Repeat;，If-then，While;，If-then-else

23、，While;，If-then-else，Repeat;，If-then與;，Repeat無法比較定義：由一組固定的基礎系構成的復合程序，稱為結構化程序。 2022/10/7華東師大計算機科學技術系482.3 結構定理證明了程序的基本結構是三種prime程序。例：只用加法操作計算兩個正整數(shù)的乘積，即：x0 y0 S z=x*yz:=0;u:=x;while u0 dobeginz:=z+y;u:=u-1;end2022/10/7華東師大計算機科學技術系49如還允許加倍、減半等操作，程序為：z:=0; u:=0; v:=0;while u0 do beginif odd(u) then z:=z+v;u:=u div 2;v:=v mul 2; end 2022/10/7華東師大計算機科學技術系50結構定理：任何一個Proper程序功能等價于基礎系;,if-then-else,while所復合的程序。證：考慮任意的Proper程序P，設P有n個結點（函數(shù)、謂詞）i）對程序中的謂詞、函數(shù)結點進行編號（1n）ii）引入一個計數(shù)器Liii）在編號的基礎上為各