茶年 · 中文维基百科

操作语义学

Wikipedia · 2026-01-03 维基百科 👁 2 阅读

操作语义学是计算机科学中的一个概念，它是使得计算机程序在数学上更加严谨的一种手段。其它类似的手段包括提供形式语义学，包括公理语义学和指称语义。

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

操作语义最早被用来定义的语义。下面这句话引用修正的报告：

一个使用严格语言编写的程序的意义是通过一个假设的计算机来执行该程序的组成部分时完成的行动来解释的。（Algol68，第二章）

丹纳·司科特是第一个在今天的这个定义下使用操作语义这个概念的（Plotkin04b）。以下是司科特关于形式语义学的讲稿，其中他提到了语义的“操作”观点。

把目光注意使得语义在更‘抽象’和更‘清晰’可以，但是假如把操作方面完全忽略的话这个计划毫无用处。（Scott70）

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

比如我们考虑一个简单计算机语言的部分语义，在Plotkin04a和Hennessy90以及其它教科书中有相应的图像。设C_1, C_2为该语言的程序域，s是状态域（即函数的存储地址及值）。假如我们有表述（E的域）、值（V）和存储地址（L），则一个存储更新指令的语义为：

\frac{\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle\longrightarrow (s\uplus (L\mapsto V))}

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

系列的语义可以用下列规则来表达：

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

假如我们还有状态的布尔函数表示B的话我们可以定义指令的语义：

\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次引用，成为计算机科学中被引用最多的技术报告之一。

参考资料

#计算机逻辑 #編程語言語義

评论 (0)

  • 还没有评论，来抢沙发吧。