語義（計算機科學）

語義描述了計算機用該特定語言執行程序時所遵循的過程。這可以通過描述程序的輸入和輸出之間的關係，或者對如何在某個平台上執行程序的說明，從而創建計算模型。

歷史

1967年，羅伯特·W·弗洛伊德（Robert W.他的主要目的是“對計算機程序的證明，包括正確性，等價和終止的證明”。弗洛伊德進一步寫道：

在我們的方法中，以句法定義建立了對編程語言的語義定義。它必須指定句法正確的程序中的哪些短語表示命令，以及在每個命令附近的解釋中必須施加哪些條件。

1969年，托尼·霍爾（Tony Hoare）發表了一篇有關弗洛伊德（Floyd）想法種子的hoare邏輯的論文，現在有時統稱為公理語義。

在1970年代，出現了操作語義和典型語義的術語。

正式語義領域包括以下所有內容：

有許多正式語義的方法；這些屬於三個主要類別：

語言語義，該語言中的每個短語都被解釋為一種表示，即可以抽像地思考的概念含義。這種表示通常是居住在數學空間的數學對象，但這並不需要它們應該這樣。作為實際的必要性，使用某種形式的數學符號來描述含義，而數學符號又可以正式化為指定的術語。例如，功能語言的典型語義通常將語言轉化為領域理論。著名的語義描述還可以用作從編程語言到示意式術語的組成翻譯，並用作設計編譯器的基礎。
操作語義，可以直接描述語言的執行（而不是通過翻譯）。操作語義很鬆散地對應於解釋，儘管解釋器的“實施語言”通常是數學形式主義。操作語義可以定義抽象的機器（例如SECD機器），並通過描述它們在機器狀態下誘導的過渡來賦予短語。或者，與純lambda演算一樣，可以通過對語言本身的短語進行句法轉換來定義操作語義。
公理語義，通過描述適用於它們的公理，可以通過描述短語的意義。公理的語義沒有區分短語的含義和描述它的邏輯公式。它的含義正是在某種邏輯中可以證明的。公理語義的規範示例是Hoare邏輯。

除了在說明，操作或公理方法之間的選擇之外，正式語義系統中的大多數變化都是由支持數學形式主義的選擇引起的。

正式語義的一些變體包括以下內容：

動作語義是一種試圖模塊化的語義語義的方法，將形式化過程分為兩層（宏觀和微觀物質），並預先定義了三個語義實體（動作，數據和產量）以簡化規範；
代數語義是一種基於代數定律的公理語義形式，用於以形式方式描述和推理程序語義。它還支持表示語義和操作語義；
屬性語法定義了系統地計算語言語法各種情況的“元數據”（稱為屬性）的系統。屬性語法可以被理解為一種表示的語義，在這種語義上，目標語言僅僅是原始語言豐富了屬性註釋。除了正式的語義外，屬性語法還用於編譯器中的代碼生成，並增加具有上下文敏感條件的常規或無上下文語法。
分類（或“函數”）語義使用類別理論作為核心數學形式主義。通常證明，分類語義與某些具有分類結構的句法表示的公理語義相對應。同樣，示意語義通常是一般分類語義的實例。
並發語義是任何描述並發計算的正式語義的術語。歷史上重要的並發形式主義包括演員模型和過程計算；
遊戲語義使用受遊戲理論啟發的隱喻；
由Edsger W. Dijkstra開發的謂詞變壓器語義將程序片段的含義描述為將後條件轉換為建立它所需的前提條件的函數。

由於各種原因，人們可能希望描述不同正式語義之間的關係。例如：

為了證明一種語言的特定操作語義可以滿足該語言的公理語義的邏輯公式。這樣的證明表明，使用特定（Axiomation）證明系統的特定（操作）解釋策略進行推理是“聲音”。
為了證明高級機器上的操作語義是通過與低級機器上的語義進行的模擬相關的，因此，低級抽像機器包含的原始操作比給定語言的高級抽像機器定義了。這樣的證明表明，低級機器“忠實地實現”了高級機器。

也可以通過抽象解釋理論通過抽象來聯繫多種語義。