查看“︁操作语义学”︁的源代码

{{Expand language|1=en|time=2020-10-22T19:19:34+00:00}}
{{模板:Semantics}}
'''操作语义学'''是[[计算机科学]]中的一个概念，它是使得[[计算机程序]]在数学上更加严谨的一种手段。其它类似的手段包括提供[[形式语义学]]，包括[[公理语义学]]和[[指称语义]]。

一个计算机语言的操作语义描述一段合理的程序是怎样被理解为一系列计算机步骤的。这些步骤就是这个程序的意义。在[[函數程式語言]]中一段终结性的序列在最后一步的返回程序的值。（由于一个程序可能是非[[非決定論|非決定的]]，一般来说一个程序能够有许多不同的计算步骤和许多不同的返回值。）

操作语义最早被用来定义{{lang|en|Algol 68}}的语义。下面这句话引用修正的{{lang|en|ALGOL 68}}报告：
<blockquote>
一个使用严格语言编写的程序的意义是通过一个假设的计算机来执行该程序的组成部分时完成的行动来解释的。（[[#algol68|Algol68]]，第二章）
</blockquote> 

丹纳·司科特是第一个在今天的这个定义下使用操作语义这个概念的（[[#plotkin04b|Plotkin04b]]）。以下是司科特关于形式语义学的讲稿，其中他提到了语义的“操作”观点。
<blockquote>
把目光注意使得语义在更‘抽象’和更‘清晰’可以，但是假如把操作方面完全忽略的话这个计划毫无用处。（[[#scott70|Scott70]]）
</blockquote>

==结构操作语义==
戈登·普罗特金（{{lang|en|Gordon Plotkin}}）在（[[#plotkin04a|Plotkin04a]]）中引入了结构操作语义的概念作为一个定义操作语义的逻辑方式。其基本主意是使用程序组成部分的行为来定义一个程序的行为，由此来提供一个对操作语义结构性的，即按照句法和归纳性的，分析。结构操作语义对一个程序的行为的说明是通过一（组）变化关系来表示的。其形式是一系列[[推理规则]]，这些推理规则通过一组句法的转换来定义该组的合理转换。

比如我们考虑一个简单计算机语言的部分语义，在[[#plotkin04a|Plotkin04a]]和[[#hennessybook|Hennessy90]]以及其它教科书中有相应的图像。设<math>C_1, C_2</math>为该语言的程序域，<math>s</math>是状态域（即函数的存储地址及值）。假如我们有表述（<math>E</math>的域）、值（<math>V</math>）和存储地址（<math>L</math>），则一个存储更新指令的语义为：
<math>
\frac{\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle\longrightarrow (s\uplus (L\mapsto V))}
</math>

使用普通语言，这个公式说'''假如'''在<math>s</math>状态的<math>E</math>的值为<math>V</math>'''则'''程序<math>L:=E</math>会通过<math>L=V</math>更新<math>s</math>的状态。

系列的语义可以用下列规则来表达：
<math>
\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}
</math>

第一个规则说假如处于状态<math>s</math>的程序<math>C_1</math>可以被简化为处于状态<math>s'</math>的程序<math>C_1'</math>的话则处于状态<math>s</math>的程序<math>C_1;C_2</math>能被简化为处于状态<math>s'</math>的程序<math>C_1';C_2</math>。第二个规则说假如处于状态<math>s</math>的程序<math>C_1</math>以状态<math>s'</math>结束的话，则处于状态<math>s</math>的程序<math>C_1;C_2</math>可以简化为处于状态<math>s'</math>的程序<math>C_2</math>。这里的语义是结构化的，因为程序序列<math>C_1;C_2</math>的意义是由<math>C_1</math>的意义和<math>C_2</math>的意义定义的。

假如我们还有状态的布尔函数表示<math>B</math>的话我们可以定义{{lang|en|while}}指令的语义：
<math>
\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}
</math>

这样的定义允许对程序行为进行公式化的分析和研究程序间的[[关系 (数学)|关系]]。

由于结构操作语义看上去非常易懂，结构简单，因此它获得了很大的欢迎，实际上成为定义操作语义的标准。结构操作语义最初的报告因此获得了约900次引用<ref>{{Cite web |url=http://citeseer.ist.psu.edu/673965.html |title=存档副本 |accessdate=2009-03-06 |archive-date=2007-03-14 |archive-url=https://web.archive.org/web/20070314223000/http://citeseer.ist.psu.edu/673965.html |dead-url=no }}</ref>，成为计算机科学中被引用最多的技术报告之一。

==参考资料==
* <cite id=algol68> {{lang|en|Adriaan van Wijngaarden}}等，《{{lang|en|Revised Report on the Algorithmic Language ALGOL 68}}》，{{lang|en|IFIP}}，1968年（[http://vestein.arb-phys.uni-dortmund.de/~wb/RR/rr.pdf]{{dead link|date=2017年12月 |bot=InternetArchiveBot |fix-attempted=yes }}）</cite>
* <cite id=plotkin04b> {{lang|en|Gordon D. Plotkin}}，《{{lang|en|The Origins of Structural Operational Semantics}}》，{{lang|en|JALP}}，60-61:3-15, 2004年（[http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf preprint] {{Wayback|url=http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf |date=20090920034629 }}）</cite>
* <cite id=scott70>  {{lang|en|Dana S. Scott}}，《{{lang|en|Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2}}》，牛津大学，1970年</cite>
* <cite id=plotkin04a> {{lang|en|Gordon D. Plotkin}}，[http://citeseer.ist.psu.edu/673965.html A Structural Approach to Operational Semantics] {{Wayback|url=http://citeseer.ist.psu.edu/673965.html |date=20070314223000 }}，（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年）([http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf preprint] {{Wayback|url=http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf |date=20090824012118 }}). </cite>
* <cite id=hennessybook>{{lang|en|Matthew Hennessy}}，《{{lang|en|Semantics of Programming Languages}}》. Wiley, 1990年. [https://web.archive.org/web/20100118143713/http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz 网上].</cite>
<references />

[[分类:计算机逻辑]]
{{Authority control}}
[[Category:編程語言語義]]