基本介紹
- 中文名：程式設計語言語義
- 外文名：programming language semantics
- 學科：計算機
- 定義：指明給出程式設計語言的程式含義
- 有關術語：語義
- 領域：程式語言
簡介,語義,操作語義,指稱語義,公理語義學,代數語義,
簡介
程式設計語言，也稱程式語言（programming language），是用來定義電腦程式的形式語言。它是一種被標準化的交流技巧，用來向計算機發出指令。程式設計語言語義為了指明給出程式設計語言的程式含義，研究語言與其所指對象間的關係。
程式設計語言語義屬於形式語義學，在計算理論中，形式語義學是關注計算的模式和程式設計語言的含義的嚴格的數學研究的領域。語言的形式語義是用數學模型去表達該語言描述的可能的計算來給出的。形式語義學（formal semantics），是程式設計理論的組成部分，以數學為工具，利用符號和公式，精確地定義和解釋電腦程式設計語言的語義，使語義形式化的學科。
語義
模型論的基本概念之一。指語言表達式和表達式的意義之間的關係。研究語義的理論稱為語義理論，又稱語義學。語義學不像語法學那樣只關心表達式的形式而不關心它們的意義。而是充分地考慮這些語言表達式在自然語言中的意義以及它們之間的關係。在語義學概念中，有真值、指派、可滿足、有效模型等概念。語義學研究系統中公式的意義、系統的解釋，且與模型論相關。語言表達式間的語義推論關係用符號⊨表示。例如，賦值語句C=A+B的語義是，把賦值號右邊的表達式A+B的值作為賦值左邊的變數C的值。在編譯過程中不但要對源程式的語法檢查其正確性，也要對語義進行檢查，保證語義上的正確。在編譯程式中，語義分析程式是由許多加工處理子程式組成，其中很重要的一部分是對標識符的處理。
操作語義
操作語義通過規定程式設計語言在抽象機器上的執行過程來描述程式設計語言的含義，即用語言的實現方式定義語言的語義，也就是將語言成分所對應的計算機操作作為語言成分的語義 。操作語義一般指結構化操作語義(SOS)，又稱“小步語義” ，其顯著特徵是：在程式運行過程中，程式短語不斷地被替換成所計算的值。這種狀態轉換可用相應的公理和推導規則來描述。SOS 已被廣泛用於程式分析和形式化驗證等領域 。與 SOS 對應的另一種操作語義為自然語義, 亦稱“大步語義” ,它較 SOS 隱藏了更多執行細節，只包含初始和最終狀態，沒有中間狀態。自然語義也用公理和推導規則描述計算, 只是它不能用於不確定的程式和交叉存取的表達式計算。自然語義已被用於定義 SML 、Eiffel 和 Java 等語言的語義。
指稱語義
在計算機科學中，指稱語義（英語：Denotational semantics）是通過構造表達其語義的(叫做指稱(denotation)或意義的)數學對象來形式化計算機系統的語義的一種方法。程式語言的形式語義的其他方法包括公理語義和操作語義。指稱語義方式最初開發來處理一個單一電腦程式定義的系統。後來領域擴展到了由多於一個程式構成的系統，比如網路和並發系統。指稱語義起源於 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初開發的時候，指稱語義把電腦程式的指稱(意義)解釋為映射輸入到輸出的函式。後來證明這對於允許包含遞歸定義的函式和數據結構這樣的元素的程式的指稱(意義)定義太受限制了。為了解決這個困難，Scott 介入了基於域的指稱語義的一般性方法(Abramsky and Jung 1994)。後來的研究者介入了基於冪域的方法，來解決並發系統的語義的問題(Clinger 1981)。
粗略的說，指稱語義關注找到代表程式所做所為的數學對象。這種對象的蒐集叫做域。例如，程式(或程式段)可以被偏函式，或演員事件圖想定，或在環境和系統之間的博弈表示: 它們都是域的一般性例子。
指稱語義的一個重要原則是“語義應當是複合性的”: 程式段的指稱應當創建自它的子段的指稱。最簡單的例子是: “3 + 4”的意義確定自“3”、“4”和“+”的意義。指稱語義最初被開發為把函式式和順序式程式建模為映射輸入到輸出的數學函式的框架。
公理語義學
公理語義學（Axiomatic semantics）是使用數理邏輯來證明程式正確性。程式中的命令的意義描述是通過對程式狀態的斷言（assertion）效果。斷言是邏輯語句——帶變數的謂詞，而這些變數定義了程式的狀態。
公理語義的套用也非常廣泛，早在 1973 年, C.A. R. Hoare 和 N. Wirth 就給出了 Pascal 完整的公理語義； 隨後,其他研究者給出了一些面向對象程式設計語言(如 Java)的核心子語言和語義網描述語言(如 XML) 的公理語義和程式驗證。
代數語義
代數語義用代數方法對形式語言系統進行語義解釋 ,即用代數公理刻畫語言成分的語義，且只研究抽象數據類型的代數規範 。抽象數據類型的代數規範通過構造運算元和一組有關運算的代數公理刻畫類型操作的行為。抽象數據類型的語法稱為基調，一個基調由它的類子集(基本語法元素)和運算集(語法元素間的組合關係)兩部分組成 。在論證這種規範滿足協調性和完全性的基礎上，通過尋找適當的模型代數，可以定義一個抽象類型的不同層次的語義，如初始語義 、 終止語義等。然後就可以用普通的代數方法論證規範的正確性和實現的正確性 。通過引入一組公理，可以為基調指定語義 。不同的公理規定不同的語義，最基本的公理形式是等式。
