操作語義學

操作語義學是計算機科學中的一個概念，它是使得電腦程式在數學上更加嚴謹的一種手段。其它類似的手段包括提供形式語義學，包括公理語義學和指稱語義。

一個計算機語言的操作語義描述一段合理的程序是怎樣被理解為一系列計算機步驟的。這些步驟就是這個程序的意義。在函數程式語言中一段終結性的序列在最後一步的返回程序的值。（由於一個程序可能是非非決定的，一般來說一個程序能夠有許多不同的計算步驟和許多不同的返回值。）

操作語義最早被用來定義Algol 68的語義。下面這句話引用修正的ALGOL 68報告：

一個使用嚴格語言編寫的程序的意義是通過一個假設的計算機來執行該程序的組成部分時完成的行動來解釋的。（Algol68，第二章）

丹納·司科特是第一個在今天的這個定義下使用操作語義這個概念的（Plotkin04b）。以下是司科特關於形式語義學的講稿，其中他提到了語義的「操作」觀點。

把目光注意使得語義在更『抽象』和更『清晰』可以，但是假如把操作方面完全忽略的話這個計劃毫無用處。（Scott70）

結構操作語義

戈登·普羅特金（Gordon Plotkin）在（Plotkin04a）中引入了結構操作語義的概念作為一個定義操作語義的邏輯方式。其基本主意是使用程序組成部分的行為來定義一個程序的行為，由此來提供一個對操作語義結構性的，即按照句法和歸納性的，分析。結構操作語義對一個程序的行為的說明是通過一（組）變化關係來表示的。其形式是一系列推理規則，這些推理規則通過一組句法的轉換來定義該組的合理轉換。

比如我們考慮一個簡單計算機語言的部分語義，在Plotkin04a和Hennessy90以及其它教科書中有相應的圖像。設${\displaystyle C_{1},C_{2}}$為該語言的程序域，${\displaystyle s}$是狀態域（即函數的存儲地址及值）。假如我們有表述（${\displaystyle E}$的域）、值（${\displaystyle V}$）和存儲地址（${\displaystyle L}$），則一個存儲更新指令的語義為： ${\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}$

使用普通語言，這個公式說假如在${\displaystyle s}$狀態的${\displaystyle E}$的值為${\displaystyle V}$則程序${\displaystyle L:=E}$會通過${\displaystyle L=V}$更新${\displaystyle s}$的狀態。

系列的語義可以用下列規則來表達： ${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

第一個規則說假如處於狀態${\displaystyle s}$的程序${\displaystyle C_{1}}$可以被簡化為處於狀態${\displaystyle s'}$的程序${\displaystyle C_{1}'}$的話則處於狀態${\displaystyle s}$的程序${\displaystyle C_{1};C_{2}}$能被簡化為處於狀態${\displaystyle s'}$的程序${\displaystyle C_{1}';C_{2}}$。第二個規則說假如處於狀態${\displaystyle s}$的程序${\displaystyle C_{1}}$以狀態${\displaystyle s'}$結束的話，則處於狀態${\displaystyle s}$的程序${\displaystyle C_{1};C_{2}}$可以簡化為處於狀態${\displaystyle s'}$的程序${\displaystyle C_{2}}$。這裡的語義是結構化的，因為程序序列${\displaystyle C_{1};C_{2}}$的意義是由${\displaystyle C_{1}}$的意義和${\displaystyle C_{2}}$的意義定義的。

假如我們還有狀態的布爾函數表示${\displaystyle B}$的話我們可以定義while指令的語義： ${\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}}$

這樣的定義允許對程序行為進行公式化的分析和研究程序間的關係。

由於結構操作語義看上去非常易懂，結構簡單，因此它獲得了很大的歡迎，實際上成為定義操作語義的標準。結構操作語義最初的報告因此獲得了約900次引用^[1]，成為計算機科學中被引用最多的技術報告之一。