基本介紹
- 中文名：程式理論
- 外文名：theory of programs
- 學科：計算機科學
- 定義：研究程式的語義和設計
- 組成：程式語義理論、數據類型理論等
- 有關術語：程式
簡介,有關理論,計算理論,
簡介
程式理論的基本問題是如何建立一個相對完善的理論框架，為軟體的設計和開發方法提供理論依據。這個框架應能提供有效地描述程式規約的語言；應能定義可操作的變換方法以便能規約構造可執行的程式；應能給出驗證程式與其規約之間一致性的機制。
有關理論
程式語義理論
程式是用程式語言編寫的，研究程式的規約、變換和驗證，必須首先給出程式語言的語義。這種語義用數學方法刻畫程式語句的加工過程，並將其執行結果形式化。所以，程式語義也叫形式語義。形式語義描述技術的本質是用嚴格的數學方法來研究程式。形式語義的研究始於20世紀60年代初期，ALGOL60 是第一個明確區分語法和語義的程式設計語言。J. McCarthyP. J.Landin，C.Strachy，D. ScottC. A. R. Hoare 和 E. W.Dijkstra 等學者，以及愛丁堡大學和維也納 IBM 研究中心的計算機科學家們對程式語義的研究和發展都起過重要作用。程式語言的形式語義分為四類: 操作語義 ，模擬程式執行中計算系統的操作過程。指稱語義，把程式作為論域間的泛函以便刻畫程式的執行數學結果。公理語義，用公理化方法刻畫程式與被加工數據的邏輯關係。代數語義，把程式執行的結果定義為滿足某種公理體系的代數結構。程式理論對形式語義的需求，促進了論域、偏序以及範疇論等數學理論的發展;而形式語義理論的研究又促進了程式語言和程式設計方法的進步，例如: 在高級語言中廣泛使用的過程說明和過程調用的精確概念和實現機制，就是在語義理論的研究中逐步明確的。
並發程式設計理論
20世70年代初期，為了保證在作業系統中多個並行執行進程的正確性，導致了並發程式理論的產生。進入80年代以來，隨著超大規模積體電路技術的日臻成熟，並行和分布計算機系統得到了迅速發展，特別是網際網路的出現和廣泛使用，大大促進了並行程式理論的發展， 使之成為程式理論的一個重要分支。並發程式是包含多個沒有因果關係的進程的程式。進程間的通信、同步和它們的並行執行是並發程式區別於順序程式的基本操作。計算機科學中的並發概念是由Petri 在1962 年提出的。Hoare 和Milner在20世紀70年代後期，分別提出並發程式的CCS和CSP 模型，他們把輸入輸出以及並行執行作為基本語法成分引入程式設計語言，並使用結構操作語義方法定義模型中基本語法成分的操作語義，開創了用代數方法研究並發程式中通信和並行行為的領域。並發程式理論研究的內容包括: 如何刻畫並行進程的行為，在什麼情況下它們可以互相模擬，研究各種通信及同步機制，以及死鎖及活性，可觀察性和發散性等並發現象。並發程式理論的研究加深了人們對並發系統的認識;其主要研究成果，例如， 關於通信和同步的概念，已作為基本語言成分在Ada，Occam和Java等程式語言中得到廣泛套用。
混合程式設計理論
進入20 世紀90年代，對控制系統的研究，例如對自動導航及核電站監測等控制系統的研究，引起了程式理論界的關注。這些系統的特點是: 它們都使用計算機進行實時控制; 對控制系統的安全性和可靠性要求高，控制系統的微小錯誤都將給經濟和社會安全帶來巨大的損失；系統中都存在兩類不同對象：根據傳統控制理論，使用微分方程刻畫的連續現象和根據邏輯或代數方法， 使用電腦程式控制的離散型事件。這類系統又叫混合系統。混合系統的程式理論已成為研究熱點。其基本目標是: 建立混合系統的計算模型，設計描述混合系統的高級語言，探索混合系統程式的設計和開發方法。在建立混合計算模型方面有三種不同的方法: 第一種稱為邏輯型混合計算模型方法，其基本思想是在時態邏輯基礎上引入時段和切變的概念。時段用於刻畫系統在時間區間上的連續變化，切變則表示系統中離散事件間的時序關係。第二種是程式設計型混合模型方法，其目標是在CSP及ADA 等並發語言中引入連續變數及給定初值的微分方程 ，而語言中原有的通信、順序及條件語句則用來表示系統中離散事件的關係。第三種方法是將自動機概念推廣，把微分方程刻畫的連續現象擴充為自動機的狀態， 用自動機狀態轉移刻畫離散事件間的關係。儘管混合系統理論發展的歷史不長， 但它在一些重要的實時控制系統中已經得到了套用，顯示出這些理論的生命力。
程式邏輯
程式邏輯是描述和論證程式行為的邏輯，又稱霍爾邏輯。程式和邏輯有著本質的聯繫。如果把程式看成一個執行過程，程式邏輯的基本方法是先給出建立程式和邏輯間聯繫的形式化方法，然後建立程式邏輯系統，並在此系統中研究程式的各種性質。用邏輯公式描述對輸入和輸出信息的要求，就可以建立邏輯公式和程式間的聯繫，表示為
其中P和Q為有關程式變元的邏輯表達式；P稱為S的前置條件；Q稱為S的後置條件。此公式表示:如果程式S執行前程式變數的值滿足前置條件P，且程式S終止，則程式S執行終止後，程式變數的值滿足後置條件Q。如果進一步建立一套關於這類公式的推理規則，就能得到一個描述程式行為的邏輯系統，可以在此系統中研究程式的性質，這就是程式邏輯。 程式是在機器中執行的，程式中每個語句的執行導致機器狀態的變化，因此程式的執行又可以由機器狀態變化的序列表達。數理邏輯中的模態邏輯正是描述動態變元變化的一種邏輯，因此以模態邏輯為基礎也可揭示邏輯與程式間的深刻聯繫。
霍爾邏輯的缺點是其基本形式不能進行邏輯演算。為了克服這種缺點，人們20世紀80年代，提出了類型論方法以求為程式的設計和開發建立更完善的理論框架。比較典型的類型 理論是由P. Martin-L f 建立的，稱為直覺主義類型論。它的基本思想是：精選一組類型(集合)作為程式規約，而它們的元素就是滿足規約的程式；用一組規則定義類型與其元素間的隸屬關係，這些規則即是從規約產生程式的變換規則，又是一階(直覺主義) 邏輯的證明規則。因此，只要對給定的規約 (邏輯命題)進行證明，就可以構造出符合此規約的程式。這樣，程式規約、變換、驗證都寓於對規約的證明之中了。
計算理論
計算理論（Theory of computation）是數學的一個領域，和計算機有密切關係。其中的理論是現代密碼協定、計算機設計和許多套用領域的基礎。該領域主要關心三個方面的問題：採用什麼計算模型（即形式語言、自動機）；解決哪些是能計算的、哪些是不能計算的（即可計算性理論及算法）；要用多少時間、要用多少存儲（即計算複雜性理論）。這三方面的問題可以用一個問題來總括：“計算機的基礎能力及限制到什麼程度？”
計算理論的“計算”並非指純粹的算術運算（Calculation），而是指從已知的輸入通過算法來獲取一個問題的答案（Computation），因此，計算理論屬於計算機科學和數學。為了對計算進行嚴謹的研究，計算機科學家會將計算以數學的方式抽象化，稱為計算模型。有幾種在使用的計算模型，其中最出名的是圖靈機。計算機科學家研究圖靈機的原因是它很容易敘述，可以分析，用來證明結果，而且用此模式呈現了許多強而有力的計算模型（引用邱奇－圖靈論題）。圖靈機有潛在的，數量無限的記憶能力，這似乎是不可能達到的，不過所有圖靈機解決的可判定性問題都只需要有限量的記憶能力。因此理論上，任何可以用圖靈機解決的（可判定性）問題都只需要有限量的記憶能力。
