操作语义学

✍ dations ◷ 2025-04-24 21:35:03 #操作语义学
操作语义学是计算机科学中的一个概念,它是使得计算机程序在数学上更加严谨的一种手段。其它类似的手段包括提供形式语义学,包括公理语义学和指称语义。一个计算机语言的操作语义描述一段合理的程序是怎样被理解为一系列计算机步骤的。这些步骤就是这个程序的意义。在函数编程语言中一段终结性的序列在最后一步的返回程序的值。(由于一个程序可能是非非决定的,一般来说一个程序能够有许多不同的计算步骤和许多不同的返回值。)操作语义最早被用来定义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次引用,成为计算机科学中被引用最多的技术报告之一。

相关

  • 癫痫持续状态癫痫重积状态(拉丁语:Status epilepticus (SE))的定义是一次癫痫发作超过五分钟、或是五分钟内癫痫发作超过一次且每次发作之间没有回复到正常状态。这种癫痫发作的状态可能是
  • 脊灰脊髓灰质炎(英语:poliomyelitis,简称polio),俗称小儿麻痹症(中文名称译自日语“小児麻痺”;后者则译自英语infantile paralysis),又译急性灰白髓炎。是由脊髓灰质炎病毒引起,可感染人
  • 嘧啶类似物嘧啶类似物(英语:Pyrimidine analogues)是与嘧啶结构上类似的核苷类似物(英语:nucleoside analogue)抗代谢物。嘧啶5-氟尿嘧啶氟尿苷吉西他滨嘧啶类抗代谢物通常通过干扰DNA的合成
  • 悲剧公地悲剧(英语:Tragedy of the commons),或共有财悲歌,是一种涉及个人利益与公共利益对资源分配有所冲突的社会陷阱。这个字起源于英国作家威廉·佛司特·洛伊(英语:William Forste
  • 6第6周期元素是元素周期表第六行(即周期)的元素,包括镧系元素。该周期元素都具有一定毒性。有:第1周期元素 - 第2周期元素 - 第3周期元素 - 第4周期元素 - 第5周期元素 - 第6周期
  • 博茨瓦纳面积以下资讯是以2014年估计家用电源国家领袖国内生产总值(购买力平价) 以下资讯是以2016年估计国内生产总值(国际汇率) 以下资讯是以2016年估计人类发展指数 以下资讯是以2018
  • 科学哲学科学哲学是20世纪兴起的一个哲学分支,关注科学的基础、方法和含义,主要研究科学的本性、科学理论的结构、科学解释、科学检验、科学观察与理论的关系、科学理论的选择等。该学
  • 胎膜羊膜囊是两层坚韧、薄、透明的膜,位于羊膜动物的胎盘之内。装着发育中的胚胎(后来变成胎儿),直到出生前不久为止。内层的膜是装着羊水和胚胎的羊膜。外层膜绒毛膜包着羊膜,本身是
  • 氰化锌氰化锌(化学式:Zn(CN)2)是锌的氰化物。白色有光泽柱状结晶或无定形块状固体或粉末。难溶于水和乙醇,微溶于热水,能溶于稀的无机酸并分解释放出氰化氢,溶于碱金属氰化物、氢氧化物
  • 论元论元(Argument),也称行动元(Actant)、项,不及物动词主语也称变元,在句法学上指句子当中具有指称功能、强制补充谓语语义的名词性成分。这些谓语往往指的是动词(V)及其助动词;名词性成