程序設(shè)計方法學(大綱) 課件

程序設(shè)計方法學ProgrammingMethodology

華東師范大學計算機科學技術(shù)系楊宗源9/15/20231華東師大計算機科學技術(shù)系程序設(shè)計方法學ProgrammingMethodology前言從方法論角度討論、研究程序設(shè)計（軟件研發(fā)）重點：程序設(shè)計的原理、原則與技術(shù)目的：提高軟件生產(chǎn)率

研究程序的性質(zhì)以及程序設(shè)計的理論和方法的學科。基本內(nèi)容一般可以包括：9/15/20232華東師大計算機科學技術(shù)系前言從方法論角度討論、研究程序設(shè)計（軟件研發(fā)）8/5/202程序的性質(zhì)與特征程序的功能描述程序的正確性驗證程序的推導與綜合程序的結(jié)構(gòu)分析程序語義的描述程序設(shè)計的策略與技術(shù)程序研制工具、

環(huán)境

涉及程序設(shè)計理論、規(guī)范、研發(fā)技術(shù)（方法）、支持環(huán)境與自動程序設(shè)計等。9/15/20233華東師大計算機科學技術(shù)系程序的性質(zhì)與特征8/5/20233華東師大計算機科學技術(shù)系授課內(nèi)容第一章綜述第二章程序的基本結(jié)構(gòu)§2.1Prime程序

§2.2復合程序

§2.3結(jié)構(gòu)定理§2.4遞歸結(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ū)ο蠓椒ā?.5面向方面編程9/15/20234華東師大計算機科學技術(shù)系授課內(nèi)容第一章綜述8/5/20234華東師大計算機科學技第四章程序的正確性證明§4.1程序規(guī)范與程序的正確性定義§4.2部分正確性證明方法§4.3完全正確性證明方法 §4.4最弱前置謂詞（WP)

第五章程序的形式推導方法 §5.1面向目標的程序設(shè)計方法

§5.2不變式推導方法

第六章程序設(shè)計的形式化方法 §6.1概述 §6.2基于代數(shù)方法的規(guī)范語言——OBJ §6.3基于模型方法的規(guī)范語言——VDM9/15/20235華東師大計算機科學技術(shù)系第四章程序的正確性證明8/5/20235華東師大計算機科第七章并行程序設(shè)計方法 §7.1基本概念

§7.2并行系統(tǒng)

§7.3并行程序設(shè)計語言

§7.4通訊順序進程(CSP)9/15/20236華東師大計算機科學技術(shù)系第七章并行程序設(shè)計方法8/5/20236華東師大計算機科學基本要求

了解程序設(shè)計方法學的地位和重要性；掌握程序控制結(jié)構(gòu)構(gòu)成的基本原理、基本成份；明確數(shù)據(jù)類型、數(shù)據(jù)抽象、抽象數(shù)據(jù)類型對程序設(shè)計及程序設(shè)計語言的影響及重要性并掌握相關(guān)技術(shù)；掌握程序正確性證明的基本方法，具有構(gòu)造程序規(guī)范的能力；理解形式化軟件開發(fā)的基本原理和典型方法；理解并行程序設(shè)計基本概念,具有并行程序設(shè)計的初步能力.9/15/20237華東師大計算機科學技術(shù)系基本要求了解程序設(shè)計方法學的地位和重要性；8/5/2023參考書

《程序設(shè)計方法學基礎(chǔ)》陳火旺湖南科學技術(shù)出版社《程序設(shè)計方法學》仲萃豪吉林大學出版社《程序設(shè)計方法學教程》張幸兒南京大學出版社《現(xiàn)代軟件工程》周之英科學出版社《形式語義學基礎(chǔ)與形式說明》屈延文科學出版社《TheScienceofProgramming》Gries,D.《CommunicatingSequentialProcessos》Hoare,C.A.R《ProgrammingfromSpecification》CarrollMorgan《程序設(shè)計方法學》胡正國國防工業(yè)出版社《對象技術(shù)導論》馮玉琳科學出版社9/15/20238華東師大計算機科學技術(shù)系參考書《程序設(shè)計方法學基礎(chǔ)》陳火旺湖南科學技術(shù)出版社第一章綜述

一、發(fā)展回顧四、五十年代 機器指令、匯編指令、FORTRAN、LISP、ALGOL語言的相繼出現(xiàn)，主要用于科學計算。 成就：馮.諾依曼 提出存儲程序 圖靈提出自動裝置的計算模型 圖靈抽象機 奠定了現(xiàn)代計算機的理論基礎(chǔ)。 評價標準： 指令條數(shù)少 存儲單元省 執(zhí)行速度快9/15/20239華東師大計算機科學技術(shù)系第一章綜述一、發(fā)展回顧8/5/20239華東師大計算機科六，七十年代 高級語言相繼出現(xiàn)，編譯技術(shù)（語言處理程序）成熟，完善，Compiler、OS、DBMS三大系統(tǒng)軟件日趨成熟，解決問題的規(guī)模，復雜性大為增加。軟件危機出現(xiàn)

缺乏宏觀上研究程序設(shè)計方法的重要性的認識?！俺绦蛟O(shè)計比人們一般想象的遠為復雜得多，其復雜程度超出了人類本身的智力、能力范圍?！?/p>

成就：

數(shù)據(jù)結(jié)構(gòu)和算法理論

程序設(shè)計=數(shù)據(jù)結(jié)構(gòu)+算法（Kunth 1971）9/15/202310華東師大計算機科學技術(shù)系六，七十年代 8/5/202310華東師大計算機科學技術(shù)系b)形式化方法運用推理、邏輯斷言等對程序的正確性進行驗證Floyd斷言法（1967） 通過斷言（謂詞公式）證明框圖程序的正確性Hoare公理化法（1969） 著名的Hoare邏輯{P}S{Q}。 通過定義一個邏輯系統(tǒng)（含有程序公理及推導規(guī)則）證明程序部分/完全正確性E.D.Dijkstra (1976)最弱前置謂詞{WP(S,Q)}S{Q}、謂詞轉(zhuǎn)換

9/15/202311華東師大計算機科學技術(shù)系b)形式化方法8/5/202311華東師大計算機科學技術(shù)系Gries 綜合了以謂詞演算為基礎(chǔ)的證明系統(tǒng)，提出了“程序設(shè)計科學”，將程序設(shè)計從經(jīng)驗、技術(shù)、技巧升華為科學。對并行程序

提出了時態(tài)邏輯、模態(tài)邏輯，刻畫安全性、事件性、優(yōu)先性、并發(fā)性等程序性質(zhì)。9/15/202312華東師大計算機科學技術(shù)系Gries 8/5/202312華東師大計算機科學技c) 軟件工程化方法——軟件開發(fā)模型1968年 北大西洋公約組織(NATO)召開軟件工程會議，首次提出用工程化方法解決軟件危機。Dijkstra（1969）提出”Goto語句”有害論。引起了討論，導致形成“結(jié)構(gòu)程序設(shè)計”的概念、原則、方法。 Pascal語言誕生（Wirth1971） i)

強調(diào)程序結(jié)構(gòu)和風格的良好性 ii)

以良好靜態(tài)結(jié)構(gòu)， 保證程序動態(tài)執(zhí)行的正確性9/15/202313華東師大計算機科學技術(shù)系c) 軟件工程化方法——軟件開發(fā)模型8/5/202313華Wirth（1971） 提出小規(guī)模程序設(shè)計和大規(guī)模程序設(shè)計本質(zhì)的不同，提出了“自頂向下、逐步細化”，“分而治之、面向功能、功能分解”的思想。Parnas（1971） 提出“信息隱藏”，模塊化。Modula-2(1979)、C（1972）、Ada（1979）UnixOS、SA、SD、JSP等等9/15/202314華東師大計算機科學技術(shù)系Wirth（1971）8/5/202314華東師大計算機科學八、九十年代編程不再是主流，構(gòu)造系統(tǒng)的方法（即系統(tǒng)的結(jié)構(gòu)、接口、集成）。網(wǎng)絡(luò)、分布式共享信息，協(xié)同工作。方法論與工程化a)

結(jié)構(gòu)化程序設(shè)計方法 80’s進入全盛時期，比較完備，稱為傳統(tǒng)方法。關(guān)系數(shù)據(jù)庫管理系統(tǒng)（RDBMS）、SQL語言趨于成熟。傳統(tǒng)的軟件工程方法： 功能分解法、數(shù)據(jù)流方法 JSD、信息造型法（E-R模型）

9/15/202315華東師大計算機科學技術(shù)系八、九十年代8/5/202315華東師大計算機科學技術(shù)系

面向?qū)ο蟪绦蛟O(shè)計方法（O-O方法） 1)

O-O是程序設(shè)計新的規(guī)范 從面向過程 面向?qū)ο? 一系列概念（如：繼承、多態(tài)、封裝……） C/C++、Eiffel、Java、C#（.NET） 2)

O-O是信息系統(tǒng)設(shè)計的方法論 面向?qū)ο蠓治?、設(shè)計（OOAD） Coad/Yourdon 面向?qū)ο蟮能浖こ?OOSE)， 用例（UseCase)建模 對象建模技術(shù)（OMT） G.BOOCH方法9/15/202316華東師大計算機科學技術(shù)系

面向?qū)ο蟪绦蛟O(shè)計方法（O-O方法）8/5/20 責任驅(qū)動設(shè)計（RDD） CRC卡（類－責任－合作） VMT（可視化建模技術(shù)）UML（統(tǒng)一建模語言UnifiedModuleLanguage)RUP（RationalUnifiedProcess)MDA（模型驅(qū)動體系結(jié)構(gòu)ModelDivenArchitechture） UML、XML、CORBA、Java3）O-O是正在興起的新技術(shù) 支持各類應用、不同種類的開發(fā)，重要的突破：軟件的復用（Reuse）、應用框架（ApplicationFrameWork)、軟件架構(gòu)（SoftwareArchitecture）

9/15/202317華東師大計算機科學技術(shù)系 責任驅(qū)動設(shè)計（RDD）8/5/202317華東師大計算機c）面向方面程序設(shè)計（Aspect-OrientedProgramming），簡稱AOP。是為解決OO方法中的問題而出現(xiàn)的。該技術(shù)被評為21世紀對經(jīng)濟和人類生活工作方式最有影響力十種技術(shù)之一。AOP的核心思想是將軟件系統(tǒng)中的橫切關(guān)注點和核心關(guān)注點分別模塊化，各自處理，再通過編織器進行無縫的編織實現(xiàn)，以解決代碼糾纏等問題，降低耦合度，提高可維護、可重用、可擴展性。目前支持AOP的語言有AspectJ、AspectC、AspectC++、AspectC#、AspectS、AspectR（Ruby）及SpringAOP、JBossAop等等。9/15/202318華東師大計算機科學技術(shù)系c）面向方面程序設(shè)計（Aspect-OrientedProd）工程化的其他方法i.

計算機輔助軟件工程（CASE） Unix工具箱、Ada的開發(fā)環(huán)境、程序綜合器、軟件工具 ii.

基于構(gòu)件（Component)的軟件工程（CBSE）COM/COM+、CORBA、EJB 設(shè)計模式(Gamma)——“其重要性可以與70年代從編程中分離數(shù)據(jù)結(jié)構(gòu)和算法作為程序設(shè)計的規(guī)律性成果相媲美”。 9/15/202319華東師大計算機科學技術(shù)系d）工程化的其他方法8/5/202319華東師大計算機

凈室軟件工程（CleanRoomSE） 集成：建模技術(shù)、形式化方法（程序驗證等）、 統(tǒng)計質(zhì)量控制等方法、技術(shù)。目的：生成極高質(zhì)量的軟件。軟件過程 CMM體系、CMMi輕載軟件工程 （Agile開發(fā)方法、敏捷軟件開發(fā)方法） eXtremeProgramming（極值編程） SCRUM開發(fā)方法 FDD（特征驅(qū)動開發(fā)方法） DSDM（動態(tài)系統(tǒng)開發(fā)方法）9/15/202320華東師大計算機科學技術(shù)系凈室軟件工程（CleanRoomSE）8/5/2023d)

形式化的方法計算機語言的研究可以分為三部分：語法學（Syntax)：研究程序設(shè)計語言的形態(tài)結(jié)構(gòu)語義學（Semantics)：研究程序設(shè)計語言和它所指的對象間的關(guān)系語用學（Pragmatics)：研究語言和它使用間的關(guān)系形式語義學四個研究領(lǐng)域、四種程序計算模型 圖靈機模型

謂詞演算模型

代數(shù)模型

遞歸函數(shù)論模型四種語義學指稱語義學 代數(shù)語義學公理語義學 操作語義學9/15/202321華東師大計算機科學技術(shù)系d)

形式化的方法8/5/202321華東師大計算機科學i)

指稱語義 采用形式系統(tǒng)方法，用相應的數(shù)學對象對一個既定形式語言的語義進行注釋的學科。其基本思想是使語言的每一成分對應于一個數(shù)學對象，該對象就稱為該語言成分的指稱，程序視為輸入域到輸出域的映射。即存在兩個域語法域：定義一個形式語言系統(tǒng)

數(shù)學域：已知語義的形式系統(tǒng)方法：用一個語義解釋函數(shù)，

以語義域中的對象值來解釋語法域中定義的語言對象的語義。基礎(chǔ)：論域理論、λ演算、不動點理論成果：VDM（TheViennaDevelopmentMethod)9/15/202322華東師大計算機科學技術(shù)系i)

指稱語義8/5/202322華東師大計算機科學技術(shù)系代數(shù)語義 用代數(shù)方法對形式語言系統(tǒng)進行語義注釋的學科基本思想是把描述語義的邏輯體系和滿足這個邏輯系統(tǒng)的各種模型統(tǒng)一在一起，并把模型的集合視為是一代數(shù)機構(gòu)，研究這些模型間的關(guān)系。基礎(chǔ)：ADT（抽象數(shù)據(jù)類型）、泛代數(shù)、范疇論方法：尋找合適的模型代數(shù)，

定義一個抽象數(shù)據(jù)類型（ADT）的不同語義，

采用代數(shù)方法論證規(guī)范的正確性和實現(xiàn)的正確性。成果：OBJ語言（代數(shù)形式化規(guī)范語言）9/15/202323華東師大計算機科學技術(shù)系代數(shù)語義8/5/202323華東師大計算機科學技術(shù)系操作語義 用機器模型語言來解釋語言的語義，基本思想是建立一個抽象機器以模擬程序在執(zhí)行過程中如何進行數(shù)據(jù)處理。 如：屬性文法除定義“做什么”（What）， 主要定義“如何做”（How）iv)

公理語義 把程序設(shè)計語言視為一個數(shù)據(jù)對象, 建立它的公理系統(tǒng)，從而使程序設(shè)計語言有了堅實的基礎(chǔ)。

9/15/202324華東師大計算機科學技術(shù)系操作語義8/5/202324華東師大計算機科學技術(shù)系這四類方法都可以形成規(guī)范語言（SpecificationLanguage），形成軟件的自動化或半自動化技術(shù)。由形成的軟件規(guī)范（由規(guī)范語言描述） 采用 演繹綜合 程序轉(zhuǎn)換 歸納綜合 過程實現(xiàn) 機器學習等不同途徑 實現(xiàn)：從形式規(guī)范到程序、從程序到程序的推導

9/15/202325華東師大計算機科學技術(shù)系這四類方法都可以形成規(guī)范語言（SpecificationL二、展望今后的發(fā)展？軟件開發(fā)對象的變化

數(shù)據(jù)處理 數(shù)據(jù) 無關(guān)信息技術(shù) 信息 與一個語境（context）相關(guān)聯(lián)9/15/202326華東師大計算機科學技術(shù)系二、展望今后的發(fā)展？8/5/202326華東師大計算機科學技知識

知識：

與多個語境相關(guān)聯(lián)

智慧 智慧：基于不同來源的已有知識 來創(chuàng)造的一般性原理9/15/202327華東師大計算機科學技術(shù)系8/5/202327華東師大計算機科學技術(shù)系第二章程序的控制結(jié)構(gòu)

§2.1Prime程序一．框圖程序的基本結(jié)點函數(shù)結(jié)點：一個入口，一個出口

與賦值語句相對應，改變了程序中變量的值。9/15/202328華東師大計算機科學技術(shù)系第二章程序的控制結(jié)構(gòu)§2.1Prime程序8/5/20控制結(jié)點（謂詞）：一個入口，兩個出口 P是謂詞，按P的值為T或F決定控制流程，不改變程序中變量的值

9/15/202329華東師大計算機科學技術(shù)系控制結(jié)點（謂詞）：一個入口，兩個出口8/5/202329華東聚合結(jié)點：二個入口，一個出口

不執(zhí)行任何運算

9/15/202330華東師大計算機科學技術(shù)系聚合結(jié)點：二個入口，一個出口8/5/202330華東師大計算在一定條件下，一個程序可由上述結(jié)點組合而成： 程序 框圖 指令 結(jié)點 控制流

有向結(jié)點網(wǎng)在框圖中將結(jié)點名去掉，則該框圖可視為一種結(jié)構(gòu)。稱為框圖結(jié)構(gòu)。例1：框圖程序：9/15/202331華東師大計算機科學技術(shù)系在一定條件下，一個程序可由上述結(jié)點組合而成：8/5/2023pf1qf29/15/202332華東師大計算機科學技術(shù)系pf1qf28/5/202332華東師大計算機科學技術(shù)系二、Proper程序

一個框圖程序，若滿足：i）一個入口，一個出口（多個出口可由聚合 結(jié)點匯聚成一個）。如：ii）每個結(jié)點總有一條從入口到出口的路徑通 過它。稱其為Proper程序。例1是Proper程序。例2：非Proper程序的例子：9/15/202333華東師大計算機科學技術(shù)系二、Proper程序一個框圖程序，若滿足：8/5/2029/15/202334華東師大計算機科學技術(shù)系8/5/202334華東師大計算機科學技術(shù)系定理：一個Proper程序，總可以歸結(jié)成一個函 數(shù)結(jié)點。證：歸結(jié)方式：找出二個（或二個以上的）結(jié)點最小的Proper程序用一個函數(shù)結(jié)點替代它直至只有一個結(jié)點為止。例3：……9/15/202335華東師大計算機科學技術(shù)系定理：一個Proper程序，總可以歸結(jié)成一個函 數(shù)結(jié)三、Prime程序

Prime程序（又稱初等程序、基本程序）

是Proper程序且其中不包括由二個以上結(jié)點組成的Proper子程序。即最小的Proper程序。例4：Prime程序有： 非Prime程序有：9/15/202336華東師大計算機科學技術(shù)系三、Prime程序Prime程序（又稱初等程序、基本程序Prime程序： 非Prime程序:9/15/202337華東師大計算機科學技術(shù)系Prime程序： 非Prime程序:8/5/202例5Prime程序的幾種重要形式：函數(shù)（func）序列（；）If-thenWhile-doppffgff9/15/202338華東師大計算機科學技術(shù)系例5Prime程序的幾種重要形式：ppffgff8/5Repeat-untilIf-then-elseDo-whilepqf

fg

f

g9/15/202339華東師大計算機科學技術(shù)系pqffgfg8/5/202339華東師大計算機科§2.2復合程序

一、程序的等價Proper程序的執(zhí)行圖（E-chart）描述Proper程序所定義的執(zhí)行路徑。E-chart的構(gòu)造法：（從Proper程序到E-chart）a）對聚合結(jié)點編號。b）以與Proper程序的入口線相連的結(jié)點為E-chart的根，并沿各路徑至出口線。9/15/202340華東師大計算機科學技術(shù)系§2.2復合程序一、程序的等價8/5/202340華東c）對E-chart中每條路徑，若當前路徑的終止結(jié)點是未曾出現(xiàn)在該路徑的結(jié)點，則把Proper程序中與此結(jié)點相連的所有出口線及其結(jié)點作為它的后繼。d）執(zhí)行路徑終止在程序的出口或回溯路徑中曾出現(xiàn)的結(jié)點。

顯然，過程終止（結(jié)點有限），得到是一棵有限樹。9/15/202341華東師大計算機科學技術(shù)系c）對E-chart中每條路徑，若當前路徑的終止結(jié)點是未曾出例6：例3中的框圖程序是Proper程序，它的 E-chart為：……

稱①②為repeat型結(jié)點，③④可以合并。Proper程序中無循環(huán)

chart圖中無repeat型結(jié)點。程序的執(zhí)行樹（E-tree）

是一棵樹，描述了程序的所有可能的執(zhí)行路徑。構(gòu)造方法： 在E-chart中將所有的Repeat型結(jié)點用相應的子樹替代，抹去所有聚合結(jié)點。

9/15/202342華東師大計算機科學技術(shù)系例6：例3中的框圖程序是Proper程序，它的8/5/202程序的等價若兩個程序有相同的E-tree，則稱它們執(zhí)行等價。若兩個程序有相同的功能，則稱它們功能等價。例7：程序與程序執(zhí)行等價pfffp9/15/202343華東師大計算機科學技術(shù)系程序的等價pfffp8/5/202343華東師大計算機科學技再如：程序程序不是執(zhí)行等價，但功能等價gpqgqp9/15/202344華東師大計算機科學技術(shù)系再如：程序gpqgqp8/5/20234結(jié)論：執(zhí)行等價=>功能等價， 但功能等價≠>執(zhí)行等價。例8：do-while是Prime程序，但其執(zhí)行等價的程序不是Prime程序ffpg9/15/202345華東師大計算機科學技術(shù)系結(jié)論：執(zhí)行等價=>功能等價，ffpg8/5/202二、復合程序一個Prime程序的函數(shù)結(jié)點用另一個Prime來替代，產(chǎn)生的一個Proper程序稱為復合程序。例9：程序是由Prime程序if-then和repeat-until復合而成的。pfq9/15/202346華東師大計算機科學技術(shù)系二、復合程序一個Prime程序的函數(shù)結(jié)點用另一個Prime來復合程序：一組固定的Prime程序（稱為基礎(chǔ)系）經(jīng)過有限次的替代運算而得到的Proper程序。將基礎(chǔ)系P1，P2…Pn所得到的復合程序全體記為{P1，P2…Pn}。復合程序集的性質(zhì)、大小由基礎(chǔ)系決定。例10：由{;,If-then}得到的程序無循環(huán)。{;，Repeat}

{;，If-then，While}{;，If-then-else，While}≡{;，If-then-else，Repeat}{;，If-then}與{;，Repeat}無法比較定義：由一組固定的基礎(chǔ)系構(gòu)成的復合程序，稱為結(jié)構(gòu)化程序。

9/15/202347華東師大計算機科學技術(shù)系復合程序：一組固定的Prime程序（稱為基礎(chǔ)系）經(jīng)過有限次的§2.3結(jié)構(gòu)定理證明了程序的基本結(jié)構(gòu)是三種prime程序。例：只用加法操作計算兩個正整數(shù)的乘積，即： {x>0∧y>0}S{z=x*y} z:=0; u:=x; whileu≠0do begin z:=z+y; u:=u-1; end9/15/202348華東師大計算機科學技術(shù)系§2.3結(jié)構(gòu)定理證明了程序的基本結(jié)構(gòu)是三種prime程序如還允許加倍、減半等操作，程序為： z:=0;u:=0;v:=0; whileu≠0do begin ifodd(u)thenz:=z+v; u:=udiv2; v:=vmul2;end9/15/202349華東師大計算機科學技術(shù)系如還允許加倍、減半等操作，程序為：8/5/202349華東師結(jié)構(gòu)定理：任何一個Proper程序功能等價于基礎(chǔ)系{;,if-then-else,while}所復合的程序。證：考慮任意的Proper程序P，設(shè)P有n個結(jié)點（函數(shù)、謂詞）i）對程序中的謂詞、函數(shù)結(jié)點進行編號（1…n）ii）引入一個計數(shù)器Liii）在編號的基礎(chǔ)上為各輸入/出線進行編號編號規(guī)則：對結(jié)點i：輸入線編號為i，輸出線為該結(jié)點后繼結(jié)點的編號；出口線為0。9/15/202350華東師大計算機科學技術(shù)系結(jié)構(gòu)定理：任何一個Proper程序功能等價于基礎(chǔ)系{;,if注：通過聚合結(jié)點至出口線的線編號為0。iv)對每個結(jié)點i構(gòu)造新結(jié)點g