形式語義學
正文
程式設計理論的組成部分。它以數學為工具，運用符號和公式，嚴格地定義程式設計語言的語義，使語義形式化，故稱形式語義學。程式設計語言是用來和計算機系統進行通信，並控制其工作的人工語言。作為語言，人工語言和自然語言（如漢語、英語等）一樣，有其語法、語義和語用範疇。程式設計語言的語法是指程式的組成規則，語義是指程式的含義；對於語用則說法不一，大致指程式的使用效果。形成和歷史 為了正確、有效地使用程式設計語言，必須了解語言中各個成分的含義，並且要求計算機系統執行這些成分所產生的效果與其含義完全一致。程式設計語言的語義通常是由設計者用一種自然語言非形式地解釋的，實施者和使用者依據各自的理解實現和使用這種語言。但是，使用自然語言和非形式的方法解釋語義，容易產生歧義現象，造成語言設計者、用戶和實施者對語義的不同理解，影響語言的正確實施和有效使用。程式設計語言中的過程調用語句就是這方面的一個典型例子。人們發現對過程調用語句的非形式的解釋可能導致各種不同的理解，產生多種不同的效果。
人們對語義精確解釋的要求產生了形式語義學，形式語義學的研究始於60年代初期,在程式設計語言ALGOL60的設計中,第一次明確區分了語言的語法和語義,並使用巴科斯－瑙爾範式成功地實現了語法的形式描述。語法的形式化大大推動了語義形式化的研究,圍繞ALGOL60的語義出現了形式語義學早期的研究熱潮。
美國史丹福大學J.麥克阿瑟於1962年系統地論述了程式設計語言語義形式化的重要性，以及它同程式的正確性、語言的正確實施等的關係，並提出在形式語義學研究中使用抽象語法和狀態向量等方法。
內容 通常的程式設計語言的語法是規定程式組成方法的一些規則，稱為具體語法，但在定義程式的語義時,必須首先識別給定的程式,分析程式的語法結構。因此，在形式語義學中使用一種討論程式分解的語法規則，這種語法稱作抽象語法。不同的程式設計語言往往使用不同的記號和表示方式。形式語義學提供的方法適用於一切程式設計語言，故抽象語法採用的記號和表示方式也是具體語法的一種抽象。
在定義程式設計語言的語義時，需要一種定義語義的語言，這種語言稱為元語言。元語言可以採用已有的數學語言，也可以是以數學理論為基礎的專門設計的語言，因此元語言的語義是嚴格的。
用程式設計語言編寫的程式，規定對計算機系統中數據的一個加工過程，形式語義學的基本方法是將程式加工數據的過程及其結果形式化，從而定義程式的語義。
由於形式化中側重面和使用的數學工具不同，形式語義學可分為四大類。①操作語義學：著重模擬數據加工過程中計算機系統的操作；②指稱語義學：主要刻劃數據加工的結果，而不是加工過程的細節；③公理語義學：用公理化的方法描述程式對數據的加工；④代數語義學：把程式設計語言看作是刻劃數據和加工數據的一種抽象數據類型,使用研究抽象數據類型的代數方法,來描述程式設計語言的形式語義。
套用和展望 形式語義學與軟體工程密切關聯，是其基礎理論之一。從形式語義學的觀點看，軟體工程中的軟體要求和軟體說明是在不同詳盡程度上對程式語義的刻劃，程式正確性是討論程式的語義和預期目標的一致；自動程式設計則是研究如何將一種元語言刻劃的程式的語義自動轉換為用另一種語言刻劃。泛函式程式設計語言和邏輯程式設計語言的研究以及根據語言的語義定義自動生成語言編譯系統的研究受到人們重視。在新一代程式設計語言的設計中，語言的形式定義將先於並指導語言的具體設計和實施，形式語義學將發揮更大的作用。
參考書目
J.McCarthy, Towards ɑ Mathematical Science of Computation, Information Processing, North-Holland Pub.,Amsterdam,1963.
