命令式语言的操作语义: 大步和小步规范的抽象描述及基于存储的语义的重写方法

理论计算机科学电子笔记174（2007）35-47www.elsevier.com/locate/entcs命令式语言FlorentKirchner1，2Francois-R′egis Sinot1，3LIX，E'colePolytechnique，91128Palaiseau，法国摘要编程语言的操作语义通常分为两种：大步和小步。 两者都是使用演绎规则定义的，其中的同余规则允许在某些上下文中进行归约。对于基于重写规则的描述，已知的方法在于导出抽象机器，这非常接近于实现。 在本文中，我们描述了命令式语言的操作语义，一种基于规则的风格，可以说和其他类型的语义学一样抽象。此外，我们结合了基于存储的语义，把重点放在内存状态，而不是值，这是更适合于命令式语言的方法。保留字：编程语言，操作语义，重写。1介绍结构操作语义（SOS）[9]已经成为定义编程语言操作意义（或语义）的标准方法尽管如此，SOS仍然允许两种不同风格的规范：大步风格定义程序和返回值之间的关系;小步风格定义程序状态之间的关系。在定义编程语言的语义时，大步长风格通常是首选的，但小步长公式有时对某些应用程序更方便（例如。，语言性质的证明[5，2]）。小步长语义旨在提供更细粒度的评估说明。非正式地说，一个小步骤的推导应该是原子的，在这个意义上，它应该是可实现的，成本与程序的大小无关。然而，传统的小步语义表示是作为演绎系统来完成的，允许演绎规则的任意高度应用在1ProjeLogical，Peol e Commund e RecherchenInformatiqueeuplatead e Saclayy，CNRS，Eol e Poly-technique，INR IA，U i versit oe Pari s-Sud.2 电子邮件：florent. inria.fr3电子邮件地址：frs@lix.polytechnique.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.02336F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35实际上，编程语言的小步表示确实是这样完成的：真正的原子步骤被描述为公理，演绎规则允许在某类上下文中进行简化。通常，该规则可以有效地应用任意次数。此外，应该允许归约的上下文类别可能非常难以定义;这是当人们试图从大步语义导出小步语义时出现的主要困难。此后，我们称这种严重依赖于上下文的表示为上下文语义第二作者最近提出了解决这些问题，对于λ-演算的各种策略，通过将小步语义描述为普通术语重写系统（TRS），而不是演绎系统或上下文术语重写系统，其中评估符号流被赋予显式状态，作为TRS语法中的标准符号，称为评估令牌。特别地，在语法级别上，将在哪里发生归约是清楚的，即在每个步骤中恰好有一个redex，其由评估令牌标记这种方法称为令牌传递语义[10，11，12]，在第3节中适用于命令式语言.传统语义学描述的另一个缺陷是强调价值，当研究对象是记忆状态时，这可能会证明是麻烦的这在命令式语言中是如此，但在证明语言中也是如此，其中状态是正在开发的证明树。在这种情况下，框架通常适用于处理程序和内存状态的配对：程序不再计算值，而是最终的内存状态，因此范式的定义需要调整。pairs的使用也在演绎规则中创造了一种人为的不对称，反映了pairs的子项本身不是pairs的事实。第一作者已经解决了这个问题，导致了基于存储的语义[4]，它将存储状态或存储置于语义的中心，因此减少直接定义在存储状态上。这解决了程序的标准形式的问题，并允许以非常直观的方式表达序列和身份的规则。有趣的是，这也允许删除上下文规则，并生成重写系统，而不是演绎规则。在第四节中对这个问题作了一些论述。我们表明，这两种方法可以结合在第5节，导致一个真正的规则为基础的语义的命令式语言，其中的评估流程（reduc- tion顺序）是明确的语法水平，并强调记忆状态。这可能被证明对于表达以状态操作为中心的语言的语义特别有用，并且对于这些语言来说，根据上下文定义求值顺序很棘手。以或多或少自动的方式从大步规范中导出小步语义和抽象机器此外，这允许借用众所周知的重写理论的结果，技术和工具。F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35372背景2.1语法我们考虑IMP风格的最小命令式语言[13]。在本说明中，重点是命令（本说明中描述的方法也可以应用于给定的一组表达式）。参考文献3XInt3n：：=0 |1 |2|......你好。.Val3v：：=真正|虚假|n|......这是什么？表达3e：：=X|v|......你好。.Com3C：：=skip|x：=e||c1;c2如果e则c1否则c2|而edoc指令3 我：：=e|Cx的范围是一个有限的参考集，e的范围是一个任意的表达式集，假设它至少包含值v。命令c包括对表达式引用的赋值'：='，用于连续应用两个命令的序列';'，表达式和命令两者的联合将被称为指令。2.2店在使用语义框架所允许的相对较高的描述水平上，我们将考虑存储器状态（或存储）是从引用到值的部分映射：σ∈Store=Ref→Val我们称σ的支持为引用集，其中σ被定义为：Supp（σ）={x∈Ref| <$v∈Val，σ（x）= v}我们还定义“为：σ38F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35nn跳过，σ跳过，σc1，σ（一）c;c，σ（B）1 2e，σx：=e，σe，σ（丙）ifethencelsec，σ（D）12e，σifethencelsec，σ（E）12e，σ当edoc时，σ跳过， σe，σ当edoc，σskip，σjj（女）（G）我们把空的存储称为映射ω∈Store，它的支持是空的，我们在存储上定义了以下操作，称为扩展：.如果y=x，σ{x<$→v}（y）=σ（y），否则。我们注意到，任何有限支集的存储都可以被描述为空存储的连续2.3大步语义学描述程序行为的最直观的方法是大步（或自然）语义，它只是程序和它们的范式之间的二元关系。它以演绎规则的形式给出，如下：i1，σ11Ni，σ其中i1，.，i，n是i的子指令，并且每个σn是σ或σJ。图1展示了IMP的大步语义。Fig. 1. IMP的Big Step语义作为一个例子，考虑在初始存储器状态ω{x<$→7}中对程序x：= 0;x：= 1的求值。然后，下面的推导产生程序的结果：F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35390，ω{x<$→ 7}x：= 0，ω{x→ 7}通过（C）1，ω{x<$→ 0}x：= 1，ω{x→ 0}通过（C）通过（B）x：= 0;x：= 1，ω{x→ 7}注意，这种形式主义反映了程序执行的一个非常粗糙的观点在某些情况下，例如当引入错误时，这并不构成足够的信息。因此，执行中的较小步骤可能需要明确说明。2.4语境语义学传统的以更原子的步骤来表达语言语义的方法被称为小步语义[7]，但我们更喜欢这里的术语上下文语义，因为我们引入的形式主义也可以被称为小步语义。甚至有人会说，这些步骤有点小。在本节中，我们将介绍改编自[7]的传统方法。表达式可能需要在存储区中查找变量，而命令可能会修改存储区。因此，用于归约的齐次符号具有以下形式：指令，存储器减少到另一对指令，存储器。 在此见证，，i，σ特别地，如果e是一个表达式，那么重复应用归约规则将得到它的范式（假设表达式的求值不会失败）：e，σ其中状态不变，v是一个值。在本说明中，重点是对命令的评估。因此，从现在开始，我们假设表达式是正确计算的，而不提供更多细节;感兴趣的读者可以参考[7]。如果c是一个命令，那么，要么它的归约不终止，要么：c，σ图2给出了命令的详细缩减规则。[]符号用于表示通常的hole概念，而Θ[i]是上下文Θ，其中hole [ ]被i替换。上一节中使用的示例计算为：x：= 0;x：= 1，ω{x<$→ 7}→ <$x：= 1，ω{x<$→ 0}<$by（b）→ ωskip，ω{x<$→1}by（a）40F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35Θ ：：=[客户端]|Θ;cI，σθ[i]，σ|x= Θ| ifΘthenc1elsec2|而Θdocx：=n，σ（一）skip;c，σ（b）第（1）款如果为真则c1elsec2，σ→c1，σ（c）第（1）款iffalse thenc1elsec2，σ（d）其他事项当b做c时，σ→ σifbthen（c;当b做c时）else skip，σ（五）图二. IMP的语境语义关于这个系统的一些评论：• 由于同余规则相对于对指令的元素的不对称性，存储器，以及跳过在范式定义中的作用，这个框架通常被认为是用于纯函数式语言的框架的特别• 这不是一个重写系统，因为在程序的表示中不允许到处发生归约这更像是一个演绎系统，其中最外层的重写规则被表示为公理，并且存在用于上下文归约的演绎规则。• 请注意，一次只能减少一次（参见[7]）。但重要的是，这一点远不明显。这依赖于有效上下文的定义和归约规则对特定实例的限制之间的紧密充分性（即， 当某些子表达式已经是标准形式时- 值或跳过）。令牌传递语义解决了其中的一些缺点。3令牌传递语义在本节中，我们将令牌传递方法从λ演算调整到我们的命令式语言的操作语义[10，11，12我们的想法是摆脱骗局-F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）3541<$σ（x：=e）→x：=（<$σe）x：=（<$σn）→ <$σ{x <$→n}skipσskip→<$σ（c1;c2）→（<$σc1）;c2（σskip）;c→（σc）σ（ifethenc1elsec2）→if（if（σtrue）thenc1elsec2→σc1if（σfalse）thenc1elsec2→σc2（一）（二）（三）（σ（whileedoc）→（IX）第一章通过允许可区分的reduction标记（即前一节中的“”，“”）在程序的语法树中以reductions而不是deductions的级别上下移动，来实现文本规则。换句话说，我们把上下文规则放在归约关系中，以一种显式的方式。为此，我们用σi和σi替换形式为i，σ的结构，取决于我们是否试图评估某个东西（在上下文中向下）或如果我们在完成某个评估之后返回一个值（在上下文中向上）。在类型方面，这两个操作符都属于Instr→Instr×Store。这给出了图3的重写规则集。图三. IMP的令牌传递语义前面的小示例说明了令牌传递重写是如何展开的：通过（IV），<$ω{x <$→7}（x：= 0;x：= 1）→（<$ω{x <$→7}x：=0）;x：=1→（<$ω{x <$→0}skip）;x：= 1 by（I）+（II）→ <$ω{x <$→0}（x：= 1）由（V）→ <$ω{x <$→1}跳过（I）+（II）我们注意到该系统的以下几点：• 该系统是作为一个普通的TRS，而不是一个演绎系统。• 语境规则以一种显式的方式被置于归约关系中。 因此，所有的步骤都是真正原子的，步骤的数量可以更合理地考虑评估的成本。例如，编译后的程序很可能不需要执行任何上下文步骤。• 如在常规方法中，一次仅存在一个可能的减少。但现在，这并不依赖于对一类上下文的微调。这是在术语级别以显式和可扩展的方式在语法上42F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35事实上，我们的方法与以前的一些作品[3，8，1]相当相似，在这些作品中，抽象机器或多或少地以系统的方式从大或小步语义中派生出来然而，我们的呈现在某种程度上更加抽象，这有利于推理，并且仍然在实现方面留下了一些自由虽然，向上的标记（σ）密切对应于上下文语义学的上下文规则的展开连续应用，但这显然是我们不介意摆脱的东西，因为它给人的印象是带有一些不确定性，在这个意义上，它的工作只是四处移动，而不是执行实际计算。第5节中给出的最终系统的情况将是非常令人高兴的。重点仍然是值：例如，赋值规则必须生成一个伪跳过命令。这看起来很像修补一个不太适合的框架。幸运的是，这个问题可以通过基于存储的语义来解决4基于存储的语义在本节中，我们将回顾基于存储的操作语义方法[4]。在基于存储的语义学中，存储器状态是形式主义的中心。我们将“”，“”符号视为一个商店构造器，并将直接在商店上执行归约。换句话说，我们定义了两个语法类别：原子存储，它等价于值，但用于存储而不是表达式，以及存储，它要么是原子的，要么是用表达式构建的。AtStore3σ٨：：=ω |σ{x <$→ v}存储3σ：：=σ٨|c，σ在 这 里， 计 算 器 的 类 型 为Com→Store→Store 。 换 句 话 说 ，我 们 有 嵌 入 式Store=Com×Store。一系列的减少是一系列的记忆状态：σ1→σ2→ ··· →σn其中，一些σi是使用，在语法上构建的，而另一些则不是。对程序的完整评估然后导致原子存储：σ→σ/→我们现在可以通过将重写规则限制到原子存储来摆脱上下文规则，这在重写系统级别上强加了一个约简策略，因此一次只能进行一次约简。中间符号，例如：=和if.然后... else，用来标记表达式的求值已经被触发，下一步应该在我们得到一个值之后发生。这个技巧有助于摆脱上下文规则。最后，我们使用[，]符号作为表达式的黑盒求值器，类型为Expr→Store→Expr。 我们也允许在表达式内部减少子表达式，尽管省略了细节。IMP的基于存储的语义是图4中提供的重写规则集。F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）3543x：=e，σx：=n，σ跳过，σ→σc1;c2，σifethenc1elsec2，σ如果为真则c1elsec2，σ→c1，σiffalsethenc1elsec2，σ当e做c时，σ_n →σ_n如果e那么（c;当e做c时）else skip，否则跳过（一）（二）（三（八）见图4。 基于存储的IMP在这里，我们的例子再次提供了关于归约系统的见解：由（iv）得到：→ ωx：= 1，ω{x<$→ 0}由（i）+（ii）由（i）+（ii）→ω{x<$→1}我们坚持认为，由此产生的系统是一个简单的术语重写系统，而不是2.4节中的演绎系统。 具体地，约简不限于给定类别的上下文。与[6]不同的是，这个系统将存储作为第一类对象处理，这避免了在某些时候引入虚拟跳过命令这解决了2.4节中的一些问题。但是，由于可能存在多个实例，因此计算顺序不是在语法上强制执行的，而是通过对原子存储的限制来强制执行的。虽然这种限制是在传统方法的哲学中，因此是完全可以接受的，但可以使用令牌传递心态对其进行改进。5基于规则的操作语义上述两种方法都有其明显的优点。因此，将它们组合到语义中是一个很自然的想法，在语义中，求值顺序在语法上是显式的，重点是存储。5.1第一枪令牌传递方法的一个重要属性是确保令牌的唯一性。如果我们更仔细地观察图4（基于存储的语义）中的序列和跳过规则，就会发现第一个规则会复制一个标记，而第二个规则会删除它。这不符合代币传递的精神。44F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35σskip→<$σ（c1;c2）→（<$σc1）c2x：=（<$σn）→ <$σ{x <$→n}相反，我们希望每个规则都只生成一个评估令牌。这给了token一个有点急切的行为：评估的结果是一个eval-uator。暂定规则见图5。跳过的规则必须返回一个令牌，所以选择很少 然后，顺序规则应该控制第一个命令，并且当第一个命令的评估完成时，它的行为与跳过规则透明。因此，序列（分号）被简单地替换为应用程序，因此评估将在处理其第一个组件后以直接的方式进行。从形式上讲，指令的语法因此扩展了令牌和隐式应用程序。图五. IMP的基于规则的操作语义，第一次尝试现在，为了计算表达式，我们不能忘记返回值，所以我们可以将其与其他令牌传递样式的规则结合起来。我们不进一步探讨这个问题，因为下面将给出一个替代方案5.2基于规则的操作语义如果我们想在同一个方向上走得更远，我们希望完全摆脱向上的标记，因为它已经是序列的情况。这个想法非常简单：我们知道如何为命令做这件事，但不知道如何为表达式做这件事，所以让我们将表达式转换为命令。更准确地说，我们将表达式转换为赋值：当我们得到一个返回值时，这个值应该作为一个可区分的变量存储在内存中，并且计算应该继续。转换在图6中非常清楚。注意，这种处理表达式的方式，即 作为命令，并不像它看起来那么牵强：2.4节的上下文语义学有一个双重方法，它把命令看作一种特殊的表达式（函数返回skip）。还可以观察到令牌具有递归类型Eval=Instr→Eval。福尔-根据这些规范，一系列（终止）归约具有以下形式：<$σc1→ ··· →（<$σc1）c2. cji→ ···→σcn−1→ πσ1我n−1nF. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）3545σ（x：=e）→（σxn→σxtrue→σσσskip→<$σ（c1;c2）→（<$σc1）c2xfalse→σ<$σ（ifxthenc1elsec2）→ <$σc1<$σ（ifxthenc1elsec2）→<$σc2σ（ifethenc1elsec2）→（x新σ（x）=trueσ（x）=false（一）（二）（三）（σ（whileedoc）→else skip）（10）见图6。 基于规则的IMP在这种形式中运行我们最喜欢的例子会产生以下推导：通过（6），得到<$ω{x <$→7}（x：= 0;x：= 1）→（<$ω{x <$→7}x：= 0）（x：= 1）xω{x<$→7}0）（x：= 1）乘（1）→ω{x <$→0}（x：= 1）由（2）xω{x<$→0}1由（1）→ω{x <$→1}由（2）请注意，我们可以添加一个特殊的命令end，其归约规则为<$σend→σ，以在评估结束时从评估令牌中提取商店。从实现的角度来看，这是有意义的，如果将JavaScript实现为一个函数。我们的形式主义在以下意义上是正确的和完整的：命题5.1 σj j使得σJ“Σ JJ。证明被省略了，但感兴趣的读者可以很容易地检查它实际上比上下文语义简单得多[7]。基于规则的操作语义确实解决了上述老式上下文语义的所有不满• 该系统是一个普通的TRS（无上下文规则）。• 我们避免了生成伪跳过命令的需要，特别是作为程序的正常形式的一部分。• 一次只能减少一次。此外，唯一的redex在语法中显式标记。与真正的令牌传递语义不同，这里的令牌总是在最左边的位置。→（→ ⇓46F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）35• 因此，它很容易实现。它也更有可能是从大步骤语义自动派生的。因此，在某种意义上，基于规则的语义可以被认为是上下文语义的对偶，以存储为中心（而不是值），并表示为重写规则（而不是演绎规则）。6结论我们已经提出了三个原始的语义框架，一个最低限度的祈使语。虽然处于比抽象机器更高的级别，但与传统方法相比，它们具有许多理想的属性这些形式主义依赖于一个更简单的模型（项重写而不是演绎系统），其中一个为评估流程提供了一个明确的状态，另一个改善了内存状态和值之间的平衡，最后一个结合了这些好处。此外，这种方法不应该太难扩展到更丰富的语言。例如，过程证明语言的语义需要处理丰富的这是正在进行的工作的主题该方法还有许多其他潜在的应用，仍有待观察。其中，重写理论的结果和工具可能更容易应用于语义学。它也是比常规方法更好的候选者，可以弥合大步规范和实现之间的差距。引用[1] 麦兹·西格·阿格。从自然语义到抽象机器。在Sandro Etalle，编辑，LOPSTR，计算机科学讲义第3573卷，第245-261页。Springer，2004.[2] 凯瑟琳·迪布瓦。Coq中ML型可靠性的证明在Mark Aagaard和John Harrison，编辑，TPHOLs，1869卷计算机科学讲义，第126-144页。Springer-Verlag，2000.[3] 约翰·汉南和戴尔·米勒抽象机器的操作语义。Mathematical Structures in Computer Science，2（4）：415[4] Fl or entKir chner.基 于 存储器的数据备份。IinSeiz i`e esJourn′eesFranc ophonesdesLangagesApplications. INRIA，2005年。[5] Gerwin Klein 和 Tobias Nipkow 。 一 个 类 似 Java 的 语 言 、 虚 拟 机 和 编 译 器 的 机 器 检 查 模 型 。 ACMTransactions on Programming Languages and Systems，2006。地出现。[6] 托拜厄斯·尼普科递归过程和无界非决定论的霍尔逻辑。J. Brad Field，编辑，Computer Science Logic（CSL 2002），计算机科学讲义第2471卷，第103-119页Springer-Verlag，2002.[7] 本杰明·皮尔斯类型和编程语言。MIT Press，2002.[8] Andrew M.皮茨 操作语义与程序等价。 In G.Barthe，P. Dybjer，J. Saraiva，editors，Applied Semantics，Advanced Lectures，Volume 2395 ofLecture Notes in ComputerScience，2004，pages 378Springer-Verlag，2002.[9] 戈登·普洛特金操作语义学的结构化方法。技术报告DAIMI FN[10] 我是说，我不是。电话号码和电话号码是一种可以在网络上进行通信的方法。在第七届类型化λ演算和应用 国 际 会 议 （ TLCA'05 ） 的 出 版 物 中 ， 计 算 机 科 学 讲 义 的 第 3461 卷 ， 第 386-400 页 。 Springer-Verlag，2005年4月F. Kirchner，F.R. Sinot/Electronic Notes in Theoretical Computer Science 174（2007）3547[11] 我是说，我不是。去网络上找：免费的电话.《电子计算机科学》，2005年。[12] 我是说，我不是。打电话给我，我会打开网络。M at he mati calStr uresinC omputerScience，16（4），2006.[13] 格林·温斯克程序设计语言的形式语义。计算机基础。MIT Press，1993.