Movatterモバイル変換

[0]ホーム
URL:

跳转到内容
维基百科自由的百科全书
搜索

操作语义学

维基百科，自由的百科全书
此條目可参照英語維基百科相應條目来扩充。(2020年10月22日)
若您熟悉来源语言和主题，请协助参考外语维基百科扩充条目。请勿直接提交机械翻译，也不要翻译不可靠、低品质内容。依版权协议，译文需在编辑摘要注明来源，或于讨论页顶部标记{{Translated page}}标签。
语义学
下屬學科
主題
分析
應用
程序語義學（英语：Semantics (computer science)）
類型
理論

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

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

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

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

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

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

结构操作语义

[编辑]

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

参考资料

[编辑]
  1. ^存档副本. [2009-03-06]. （原始内容存档于2007-03-14）. 
规范控制数据库：各地編輯維基數據鏈接
检索自“https://zh.wikipedia.org/w/index.php?title=操作语义学&oldid=62495479”
分类：​
隐藏分类：​
[8]ページ先頭
©2009-2025 Movatter.jp