程序設計方法學

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

程序設計方法學發展歷史[編輯]

產生背景[編輯]

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的謂詞轉換器及其演算規則集合，可以推導出正確的程序。

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

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

抽象數據類型的研究[編輯]

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

研究的內容[編輯]

與軟件工程的關係[編輯]

研究方法的不同[編輯]

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

研究的對象不同[編輯]

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