首页 >
操作语义学
✍ dations ◷ 2024-07-05 02:55:42 #操作语义学
操作语义学是计算机科学中的一个概念,它是使得计算机程序在数学上更加严谨的一种手段。其它类似的手段包括提供形式语义学,包括公理语义学和指称语义。一个计算机语言的操作语义描述一段合理的程序是怎样被理解为一系列计算机步骤的。这些步骤就是这个程序的意义。在函数编程语言中一段终结性的序列在最后一步的返回程序的值。(由于一个程序可能是非非决定的,一般来说一个程序能够有许多不同的计算步骤和许多不同的返回值。)操作语义最早被用来定义Algol 68的语义。下面这句话引用修正的ALGOL 68报告:一个使用严格语言编写的程序的意义是通过一个假设的计算机来执行该程序的组成部分时完成的行动来解释的。(Algol68,第二章)丹纳·司科特是第一个在今天的这个定义下使用操作语义这个概念的(Plotkin04b)。以下是司科特关于形式语义学的讲稿,其中他提到了语义的“操作”观点。把目光注意使得语义在更‘抽象’和更‘清晰’可以,但是假如把操作方面完全忽略的话这个计划毫无用处。(Scott70)戈登·普罗特金(Gordon Plotkin)在(Plotkin04a)中引入了结构操作语义的概念作为一个定义操作语义的逻辑方式。其基本主意是使用程序组成部分的行为来定义一个程序的行为,由此来提供一个对操作语义结构性的,即按照句法和归纳性的,分析。结构操作语义对一个程序的行为的说明是通过一(组)变化关系来表示的。其形式是一系列推理规则,这些推理规则通过一组句法的转换来定义该组的合理转换。比如我们考虑一个简单计算机语言的部分语义,在Plotkin04a和Hennessy90以及其它教科书中有相应的图像。设
C
1
,
C
2
{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,srangle Rightarrow V}{langle L:=E,,,srangle longrightarrow (suplus (Lmapsto V))}}}使用普通语言,这个公式说假如在
s
{displaystyle s}
状态的
E
{displaystyle E}
的值为
V
{displaystyle V}
则程序
L
:=
E
{displaystyle L:=E}
会通过
L
=
V
{displaystyle L=V}
更新
s
{displaystyle 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
,
s
′
⟩
⟨
s
k
i
p
,
s
⟩
⟶
s
{displaystyle {frac {langle C_{1},srangle longrightarrow langle C_{1}',s'rangle }{langle C_{1};C_{2},,srangle longrightarrow langle C_{1}';C_{2},,s'rangle }}quad {frac {langle C_{1},srangle longrightarrow s'}{langle C_{1};C_{2},,srangle longrightarrow langle C_{2},s'rangle }}quad {frac {}{langle mathbf {skip} ,srangle longrightarrow s}}}第一个规则说假如处于状态
s
{displaystyle s}
的程序
C
1
{displaystyle C_{1}}
可以被简化为处于状态
s
′
{displaystyle s'}
的程序
C
1
′
{displaystyle C_{1}'}
的话则处于状态
s
{displaystyle s}
的程序
C
1
;
C
2
{displaystyle C_{1};C_{2}}
能被简化为处于状态
s
′
{displaystyle s'}
的程序
C
1
′
;
C
2
{displaystyle C_{1}';C_{2}}
。第二个规则说假如处于状态
s
{displaystyle s}
的程序
C
1
{displaystyle C_{1}}
以状态
s
′
{displaystyle s'}
结束的话,则处于状态
s
{displaystyle s}
的程序
C
1
;
C
2
{displaystyle C_{1};C_{2}}
可以简化为处于状态
s
′
{displaystyle s'}
的程序
C
2
{displaystyle C_{2}}
。这里的语义是结构化的,因为程序序列
C
1
;
C
2
{displaystyle C_{1};C_{2}}
的意义是由
C
1
{displaystyle C_{1}}
的意义和
C
2
{displaystyle C_{2}}
的意义定义的。假如我们还有状态的布尔函数表示
B
{displaystyle B}
的话我们可以定义while指令的语义:
⟨
B
,
s
⟩
⇒
t
r
u
e
⟨
w
h
i
l
e
B
d
o
C
,
s
⟩
⟶
⟨
C
;
w
h
i
l
e
B
d
o
C
,
s
⟩
⟨
B
,
s
⟩
⇒
f
a
l
s
e
⟨
w
h
i
l
e
B
d
o
C
,
s
⟩
⟶
s
{displaystyle {frac {langle B,srangle Rightarrow mathbf {true} }{langle mathbf {while} B mathbf {do} C,srangle longrightarrow langle C;mathbf {while} B mathbf {do} C,srangle }}quad {frac {langle B,srangle Rightarrow mathbf {false} }{langle mathbf {while} B mathbf {do} C,srangle longrightarrow s}}}这样的定义允许对程序行为进行公式化的分析和研究程序间的关系。由于结构操作语义看上去非常易懂,结构简单,因此它获得了很大的欢迎,实际上成为定义操作语义的标准。结构操作语义最初的报告因此获得了约900次引用,成为计算机科学中被引用最多的技术报告之一。
相关
- 抗原抗原(antigen,缩写Ag)为任何可诱发免疫反应的物质,不只是从病原体那里取得,一般来说体内发现分子够大的有机物就有可能作为一个适合的抗原,这样也就会导致例如过敏等问题。外来分
- 军团病军团病,又名退伍军人症是由军团菌引发的非典型肺炎。 其症状包括咳嗽、呼吸困难、发热、肌肉疼痛、头痛。有时亦会发生恶心、呕吐、腹泻。军团病的症状通常在暴露后两到十天
- 罗萨林·耶洛罗莎琳·萨斯曼·耶洛(英语:Rosalyn Sussman Yalow,1921年7月19日-2011年5月30日),美国医学物理学家,因开发多肽类激素的放射免疫分析法,而与罗歇·吉耶曼和安德鲁·沙利共同获得197
- 氯霉素氯霉素(Chloramphenicol)是一种抗生素,可用于治疗许多细菌感染症状,包括脑膜炎、瘟疫、霍乱和伤寒等。只有在不能使用其他较安全的抗生素时,才会建议用氯霉素。治疗期间,建议每两
- 坏死坏死(英语:Necrosis),又称细胞坏死,被认为是一种由外部或内部物理性因素(例如热力、应力和辐射等)、强碱、强酸及毒物等化学性因素,以及内毒素和病原体等生物性因素诱发的永久性细胞
- 芽枝霉门异水霉属 Allomyces 芽枝霉属 Blastocladia 雕蚀菌属 Coelomomyces芽枝霉门是真菌中的一门,生存于土壤及淡水之中,且绝大部分为腐生。芽枝霉门有一纲、一目、五科。其中的三
- 隐球菌线黑粉菌属 Filobasidiella隐球菌属(学名:Cryptococcus,字面的意思是“隐藏的球体”)是担子菌门下的一个属,其下物种为单细胞的酵母菌型。隐球菌属物种的菌丝形态常用线黑粉菌属(F
- 七宗罪七宗罪(拉丁语:septem peccata mortalia;英语:seven deadly sins),天主教称七罪宗,或称七大罪或七原罪,属于天主教教义中对人类恶行的分类。归入这一类别的,能够直接形成其他不道德的
- 舌舌(舌头)是口腔底的肌肉,帮助咀嚼、吞咽、构音和感受味觉。舌能辨别酸、甜、苦、辣、咸、鲜味,舌表面的大部分粘膜上皮中含味蕾。因为舌是帮助发声的器官之一,在一些语言中,比如在
- 污染物排放控制技术污染物排放控制基本从三个方面开发:第一种方法是目前最常用的方法,但需要投入并没有经济效益,采取这种方法肯定会增加生产成本,降低产品竞争力,一般污染物排放单位不会自动处理,必