程式設計方法學[學科]

程式設計方法學是討論程式的性質以及程式設計的理論和方法的一門學科， 是研究和構造程式的過程的學問，是研究關於問題的分析，環境的模擬，概念的獲取，需求定義的描述， 以及把這種描述變換細化和編碼成機器可以接受的表示的一般的方法。

介紹

用以指導程式設計各階段工作的原理和原則，以及依此提出的設計技術。有時也指研究這些原理、原則和技術的學科。程式設計方法學的目標是能設計出可靠、易讀而且代價合理的程式。程式設計方法學包括程式理論、研製技術、支援環境、工程規範和自動程式設計等課題，使程式設計更加科學化和工程化。其基本內容是：結構程式設計；程式理論在程式設計技術中的套用，以及規格說明和變換技術。程式理論與程式設計方法學的發展密切相關，它豐富了程式人員的思維方法，促進了程式設計技術的發展。

發展歷史

產生背景

1950年代—1960年代初，手工藝式的程式設計方法，高德納把程式稱為藝術品。

1960年代末—1970年代初，出現軟體危機：一方面需要大量的軟體系統，如作業系統、資料庫管理系統； 另一方面，軟體研製周期長，可靠性差，維護困難。編程的重點：希望編寫出的程式結構清晰、易閱讀、易修改、易驗證，即得到好結構的程式。

1968年，北大西洋公約組織（NATO）在西德召開了第一次軟體工程會議，分析了危機的局面，研究了問題的根源，第一次提出了用工程學的辦法解決軟體研製和生產的問題，本次會議可以算做是軟體發展史上的一個重要的里程碑。

1969年，國際信息處理協會（IFIP）成立了“程式設計方法學工作組”，專門研究程式設計方法學，程式設計從手工藝式向工程化的方法邁進。

結構化研究

1968 年，結構化程式設計方法的研究。Dijkstra 提出了“GOTO是有害的”，希望通過程式的靜態結構的良好性保證程式的動態運行的正確性。

1969 年，Wirth 提出採用“ 自頂向下逐步求精、分而治之” 的原則進行大型程式的設計。其基本思想是：從欲求解的原問題出發，運用科學抽象的方法，把它分解成若干相對獨立的小問題，依次細化，直至各個小問題獲得解決為止。

“ 程式正確性證明”

1967年，Floyd 提出用“ 斷言法” 證明框圖程式的正確性。

1969年，Hoare 在Floyd 的基礎上，定義了一個小語言和一個邏輯系統。此邏輯系統含有程式公理和推導規則，目的在於證明程式的部分正確性，這就是著名的Hoare邏輯。他的工作為公理學語義的研究奠定了基礎。

1973年，Hoare和Wirth把PASCAL語言的大部分公理化。

1975年，一個基於公理和推導規則的自動驗證系統首次出現。

1979年，出現了用公理化思想定義的程式設計語言Euclid。

1976年，Dijkstra提出了最弱前置謂詞和謂詞轉換器的概念，用於進行程式的正確性證明和程式的形式化推導。

1980年，D.Gries綜合了以謂詞演算為基礎的證明系統，稱之為“程式設計科學”。首次把程式設計從經驗、技術升華為科學。

1974年，人們利用模態邏輯驗證並行程式的正確性。

關於程式正確性證明的爭論：

懷疑和反對派,理由：首先，形式證明太複雜，誰能夠保證證明本身沒有錯誤呢！其次，程式寫好後再證明其正確性，相當於“ 馬後炮” ，即錯誤已經鑄成，證明何能補救？

折中的方案：編寫程式，邊考慮證明。即程式設計與正確性證明同時並行考慮。

構造正確的程式

利用Dijkstra 的謂詞轉換器及其演算規則集合，可以推導出正確的程式。

利用程式變化構造正確的程式。它對程式套用一連串的保護正確性的變換規則，最終得到可執行的程式。程式變換是1970年代以來，“程式設計方法學” 研究的重要方面，是程式設計自動化很有希望的途徑之一。遞歸程式變換是這一時期的最有意義的成果。 如Burstall 和Darlington 的遞歸程式變換系統等。

邏輯程式設計和函式程式設計代表一種新的研究方向。Prolog是以謂詞邏輯的子集（Hoare 子句）為基礎的一種形式系統。Prolog 的執行過程就是執行邏輯上消解算法的過程。

抽象數據類型的研究

抽象數據類型是程式設計方法學中一種極為重要的方法。人們把它譽為程式設計方法學發展史上的一個重要的里程碑。

研究的內容

結構化程式設計

數據抽象與模組化程式設計

程式正確性證明

程式變換

程式的形式說明與推導

程式綜合與分析技術

面向對象的程式設計方法

大型程式的開發

與軟體工程的關係

程式設計方法學也與軟體工程關係密切。方法學對軟體的研製和維護起指導作用。軟體工程要求程式設計規範化，建立新的原則和技術。而一種新的方法的出現，又要求制訂出相應的規範。方法和工具是同一問題的兩個側面。工具的研究以方法學為基礎，而工具的研製成功又會影響程式設計。程式設計方法學還涉及程式推導、程式綜合、程式設計自動化研究、並發程式設計、分散式程式設計、函式式程式設計、語義學、程式邏輯、形式化規格說明和公理化系統等課題。

研究方法的不同

軟體工程主要套用工程的方法和技術研究軟體開發與維護的方法、工具和管理的一門計算機科學與工程學交叉的學科 程式設計方法學主要運用數學方法研究程式的性質以及程式設計的理論和方法的學科；

研究的對象不同

軟體工程的研究對象是軟體系統。目標是降低軟體的開發成本，提高軟體的質量，提高軟體的可維護性，提高軟體開發的效率。著重於軟體的巨觀可用性。程式設計方法學研究對象是程式。目標是保證程式的正確性。著重於程式的微觀正確性。軟體工程與程式設計方法學的界限變得越來越模糊 程式設計方法學是軟體工程的基礎。