操作语义学
结构操作语义
戈登·普罗特金(Gordon Plotkin)在(Plotkin04a)中引入了结构操作语义的概念作为一个定义操作语义的逻辑方式。其基本主意是使用程序组成部分的行为来定义一个程序的行为,由此来提供一个对操作语义结构性的,即按照句法和归纳性的,分析。结构操作语义对一个程序的行为的说明是通过一(组)变化关系来表示的。其形式是一系列推理规则,这些推理规则通过一组句法的转换来定义该组的合理转换。
比如我们考虑一个简单计算机语言的部分语义,在Plotkin04a和Hennessy90以及其它教科书中有相应的图像。设C1,C2{\displaystyle C_{1},C_{2}}为该语言的程序域,s{\displaystyle s}是状态域(即函数的存储地址及值)。假如我们有表述(E{\displaystyle E}的域)、值(V{\displaystyle V})和存储地址(L{\displaystyle L}),则一个存储更新指令的语义为: ⟨ ⟨ -->E,s⟩ ⟩ -->⇒ ⇒ -->V⟨ ⟨ -->L:=E,s⟩ ⟩ -->⟶ ⟶ -->(s⊎ ⊎ -->(L↦ ↦ -->V)){\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}
使用普通语言,这个公式说假如在s{\displaystyle s}状态的E{\displaystyle E}的值为V{\displaystyle V}则程序L:=E{\displaystyle L:=E}会通过L=V{\displaystyle L=V}更新s{\displaystyle s}的状态。
系列的语义可以用下列规则来表达: ⟨ ⟨ -->C1,s⟩ ⟩ -->⟶ ⟶ -->⟨ ⟨ -->C1′,s′⟩ ⟩ -->⟨ ⟨ -->C1;C2,s⟩ ⟩ -->⟶ ⟶ -->⟨ ⟨ -->C1′;C2,s′⟩ ⟩ -->⟨ ⟨ -->C1,s⟩ ⟩ -->⟶ ⟶ -->s′⟨ ⟨ -->C1;C2,s⟩ ⟩ -->⟶ ⟶ -->⟨ ⟨ -->C2,s′⟩ ⟩ -->⟨ ⟨ -->skip,s⟩ ⟩ -->⟶ ⟶ -->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}}}
第一个规则说假如处于状态s{\displaystyle s}的程序C1{\displaystyle C_{1}}可以被简化为处于状态s′{\displaystyle s"}的程序C1′{\displaystyle C_{1}"}的话则处于状态s{\displaystyle s}的程序C1;C2{\displaystyle C_{1};C_{2}}能被简化为处于状态s′{\displaystyle s"}的程序C1′;C2{\displaystyle C_{1}";C_{2}}。第二个规则说假如处于状态s{\displaystyle s}的程序C1{\displaystyle C_{1}}以状态s′{\displaystyle s"}结束的话,则处于状态s{\displaystyle s}的程序C1;C2{\displaystyle C_{1};C_{2}}可以简化为处于状态s′{\displaystyle s"}的程序C2{\displaystyle C_{2}}。这里的语义是结构化的,因为程序序列C1;C2{\displaystyle C_{1};C_{2}}的意义是由C1{\displaystyle C_{1}}的意义和C2{\displaystyle C_{2}}的意义定义的。
假如我们还有状态的布尔函数表示B{\displaystyle B}的话我们可以定义while指令的语义: ⟨ ⟨ -->B,s⟩ ⟩ -->⇒ ⇒ -->true⟨ ⟨ -->while B do C,s⟩ ⟩ -->⟶ ⟶ -->⟨ ⟨ -->C;while B do C,s⟩ ⟩ -->⟨ ⟨ -->B,s⟩ ⟩ -->⇒ ⇒ -->false⟨ ⟨ -->while B do C,s⟩ ⟩ -->⟶ ⟶ -->s{\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次引用,成为计算机科学中被引用最多的技术报告之一。
参考资料
Adriaan van Wijngaarden等,《Revised Report on the Algorithmic Language ALGOL 68》,IFIP,1968年([2])
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年.网上.
免责声明:以上内容版权归原作者所有,如有侵犯您的原创版权请告知,我们将尽快删除相关内容。感谢每一位辛勤著写的作者,感谢每一位的分享。
- 有价值
- 一般般
- 没价值