操作语义学

戈登·普罗特金（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]，成为计算机科学中被引用最多的技术报告之一。

• Adriaan van Wijngaarden等，《Revised Report on the Algorithmic Language ALGOL 68》，IFIP，1968年（[1]^{[永久失效链接]}）
• Gordon D. Plotkin，《The Origins of Structural Operational Semantics》，JALP，60-61:3-15, 2004年（preprint （页面存档备份，存于互联网档案馆））
• Dana S. Scott，《Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2》，牛津大学，1970年
• Gordon D. Plotkin，A Structural Approach to Operational Semantics （页面存档备份，存于互联网档案馆），（1981年），Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139（2004年）(preprint （页面存档备份，存于互联网档案馆）).
• Matthew Hennessy，《Semantics of Programming Languages》. Wiley, 1990年. 网上.

1. ^ 存档副本. [2009-03-06]. （原始内容存档于2007-03-14）.