编程语言的形式语义：理论与实践

理论计算机科学电子笔记148（2006）41-73www.elsevier.com/locate/entcs程序设计语言- 概述-Peter D. 苔藓1英国威尔士大学斯旺西分校计算机科学系摘要这些注释概述了为指定编程语言的形式语义而开发的主要框架。一些实用方面的语义去重的讨论，包括模块化，和潜在的适用性可视化和建模语言。参考文献为进一步研究提供了起点。关键词：语义，操作语义，指称语义，SOS，MSOS，归约语义，抽象状态机，一元语义，公理语义，动作语义，编程语言，建模语言，可视化语言1引言一个程序设计语言的语义学为每个程序的计算意义建模。一个程序的计算意义当一个程序在某个真实的计算机上执行时实际发生的事情太复杂而不能完整地描述。相反，编程语言的语义提供了抽象实体，这些实体只表示所有可能执行的相关特征通常，唯一被认为是相关的特性是输入和输出之间的关系，以及执行是否终止1电子邮件：p.d. swansea.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.01242警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41或不.具体到实现的细节，例如存储变量值的实际机器地址，“垃圾收集”的可能性程序的形式和结构是由它们的语法决定的在我们开始给一种编程语言赋予语义之前，我们需要对这种语言所允许的程序的形式和结构有一个精确的定义。一种语言的语法不仅决定了程序是否合法，还决定了它的内部分组结构。D描述被称为正式的时候写在一个符号已经有一个精确的含义。编程语言的参考手册和标准通常提供程序语法的正式描述，用BNF的某些变体编写。然而，考虑到语言的计算意义，参考手册中的描述通常是完全非正式的，仅用自然语言表达，即使非常学究式地使用，也本质上是不精确的，容易引起误解。1.1语法编程语言有几种语法：具体的，抽象的，规则的，上下文无关的和上下文相关的。程序设计语言的具体语法包括文本和解析。具体语法确定哪些文本字符串被接受为程序，并为每个接受的程序提供一个解析树，指示应该如何对文本进行分组。具体语法通常由形式语法指定，产生式为每个非终结符提供了一组替代项具体语法的语法应该是明确的，这样每个被接受的程序都有一个唯一的解析树;另一种方法是让语法保持不明确，并提供优先规则来选择唯一的解析树。表1显示了一个语法片段，它可以用来指定ML的具体语法。语法是用BNF的一个变体编写的，使用正则表达式的符号来描述数字和标识符。22在符号之间隐式地允许布局字符警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4143表1混凝土浇筑exp-->“if”exp“then”exp“else”exp|......这是什么？|......这是什么？|... |atexpatexp --> const |ID|......这是什么？const --> bool |int|“（）”bool -->“true”|“false”int -->[0-9]+id-->[A-Za-z][A-Za-z0-9]*建模语言的具体语法通常包括文本和图形符号的混合尽管程序通常是以文本形式编写的，但软件模型是通过大量使用包含框、线和箭头的图表来公式化的[30]。这些图表是以非串行方式交互创建的每个图也有一个纯文本的序列表示，但这主要用作工具之间的交换格式，而不是用于创建图。图的具体语法可以被指定为一组类似于文本语法的规则，尽管关于连接点和二维布局的细节必须明确，这使事情变得相当复杂。模块化和重用在描述具体语法时是有用定义形式主义（SDF）[9]允许将具体语法的描述划分为具有显式依赖的模块人们可能期望指定各种低级构造（如布尔、整数和标识符）的模块然而，指定特定构造集合的模块ML中的表达式）通常只能在描述语言扩展时不加更改地重复使用D抽象语法只处理结构。具体语法处理用于编写程序的实际字符串，而抽象语法只关心程序的在抽象语法树中，每个节点由特定的构造函数创建，并且对于其构造函数的每个参数都有一个分支。除了没有参数的构造函数之外，树的叶子可以包括与诸如数字和标识符之类的法律符号相对应的字符序列;我们还可以考虑所谓的增值抽象语法树，其中抽象数学实体（真值-44警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41表2摘要Exp：：= cond（Exp，Exp，Exp）|赋值（Exp，Exp）|Const |ID|......这是什么？Const：：= Bool|Int|null Id ：：= String值、数字、甚至诸如加法之类的操作）被允许作为叶子。D抽象语法可以用各种方式来指定抽象语法的基本方面是节点的构造器，以及将节点分类为（可能重叠的）集合。这些具体如何举例来说• 作为数据类型定义（如ML中所见），可能也允许子类型定义（如CASL[27]）;• 使用面向对象的技术和符号（如UML [30]）;或• 通过简单地指出每个构造函数的参数和结果类型表2中给出的规范使用了类似于CASL中提供的数据类型定义的语法符号特定的抽象语法表示表1中用于说明具体语法的相同表达式的深层结构。D抽象语法可以自由选择在指定抽象语法时，必须做出各种选择，例如：使用哪些符号作为类型和构造函数的名称;何时将类似的构造分组为可区分的类型;以及是否保留由字符序列表示的词汇构造，或将其替换为相应的通常，这些选择然而，使抽象语法尽可能独立于语言，有利于在另一种语言中重用一种语言的语义描述的部分例如，可以选择类型和构造函数的符号来反映编程构造的非正式讨论中使用的正常词汇，例如表达式（abbr. 后一个符号也避免了暗示条件表达式的任何特定的具体语法：如果我们选择了，比如说，：警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4145表3Prolog中具体语法到抽象语法的映射exp（cond（E1，E2，E3））“if”，exp（E1），“then”，exp（E2），“else”，exp（E3）.exp（E）--> infexp（E）.infexp（assign（E1，E2））--> atexp（E1），“：="，atexp（E2）....在表2中，标准数学集合Bool（由布尔真值true和false组成，配备有否定、合取、析取等），假设给定了Int（整数）和String，以及它们的操作和关系的常规符号。抽象语法通常比具体语法简单得多请注意，在抽象语法中，ex-expression、in fix expressionsinfexp和atomicexpressionsatexp的具体非终结符之间的区别是如何被消除的这使得抽象语法树的结构比对应具体语法的解析树的这种泛化使得抽象语法比具体语法简单得多，并且使其特别适合用作语法和语义之间的接口D完整的描述指定了具体和抽象的语法。完整的语言描述应该提供具体和抽象语法，并指定从程序文本到抽象语法树的预期映射。当使用定义子句文法（如Prolog提供的）来指定具体语法时，抽象语法树的构造可以在语法本身中指定，如表3所示。D抽象语法树可以直接构造对于程序员来说，以交互方式构造程序的抽象语法树是可能的（但相对乏味），就像在建模语言中构造具体图一样。但即使这样，为了显示程序，仍然需要一个文本化的具体语法从抽象语法树到文本形式的在哪里插入换行符和缩进的实用问题使漂亮印刷的正式描述变得复杂46警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41D当具体语法是可视的时，抽象语法图可能更合适编程语言的抽象语法是基于树的。 这部分是因为抽象语法来自程序的解析树。然而，标识符的声明和使用确实会产生一个隐式的图结构，如果需要的话，可以显式化对于具体语法主要基于图的语言，例如可视化建模语言，抽象语法图似乎比树更合适[3]。当图涉及未命名的组件时，情况尤其如此：转换为树可能需要为这些组件创建唯一的标签（例如，当多个箭头指向匿名连接点时[8]）。请注意，树比图有相当大的理论优势，因为（有限）树允许归纳定义。这是指称语义的一个重要特征，对于通过结构归纳证明操作语义的性质具有重要意义D上下文无关语法处理分组。编程语言中的分组规则通常是固定的，因此分组分析与上下文无关。然而，一些语言（包括ML）允许在程序中指定in fix和prefix运算符的优先级，并且这些语言中的表达式分组显然是上下文敏感的。由于抽象语法树仅在分组已经确定之后才构造，因此抽象语法不受分组分析问题的影响。D上下文相关语法也可以处理约束。诸如使用前声明和类型检查约束之类的格式良好条件本质上是上下文敏感的，并且不能由上下文无关语法指定。满足这些良构性条件的程序的抽象语法可以被看作是抽象语法的一个子集，其中的条件被忽略。1.2语义语义有几个层次：静态语义、动态语义和等价。D静态语义模型编译时检查。当（抽象）语法被限制为与上下文无关时，检查程序是否警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4147抽搐它被称为静态语义，因为它只涉及那些可以在运行程序之前执行的检查，例如检查程序的所有部分都是类型正确的。程序的静态语义的唯一相关特征是程序是否通过了检查（尽管编译器发出的错误报告可以建模，当这些错误报告与实现无关时）。动态语义模型运行时行为。动态语义关注程序运行时可观察到的行为在这里，我们可以假设程序的良构性已经被静态语义检查过了：我们不需要考虑病态程序的动态语义。程序之间的等价性可以从模型的细节中抽象出来。一个形式化的语义应该为每个程序给出一个抽象的模型，这个模型只表示该程序所有可能执行的相关特征当两个程序的模型相同（直到同构）时，它们被认为是语义等价的。另一种方法是给出不那么抽象的模型，然后为每个模型定义一个语义等价关系。完整的描述包括静态语义、动态语义和语义等价。给定一个被上下文无关的具体语法接受的程序，需要一个静态然后，动态语义提供了一个程序执行的模型。语义等价关系从那些与实现正确性无关的特征中抽象出来所有这些共同提供了给定程序的完整语义。D这些注释关注动态语义，基于上下文无关的抽象语法。动态语义有几种主要的方法• 操作语义，其中计算被显式地建模• 指称语义，其中仅对每个构造对封闭程序的计算意义的贡献进行建模;以及• 公理语义学，它（实际上）对程序变量的前置条件和后置条件之间的关系进行建模。48警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41结构化操作语义[31]是简单性和实用性之间的一个很好的折衷，它已被广泛教授在本科水平[10，29，37，41]。SOS的一个模块化变体MSOS [26]相对于原始SOS框架具有一些显著的实用优势，但在概念上仍然非常接近。称为动作语义[21，28，40]的混合框架-不要与UML动作语义混淆-结合了表示和操作语义的特征。现在让我们概述一下主要的语义框架。对于每个框架，其目的是解释其主要原则，给出语义描述在其中的印象，并提请注意它可能存在的任何主要缺点参考文献为进一步研究提供了起点2结构操作语义学结构操作语义学（Structural Operational Semantics，SOS）是由Plotkin在1981年提出的。其主要目的是提供一种简单而直接的方法，允许基于初等数学的简洁和可理解的语义描述。SOS的基本框架已经在各种教科书中提出（例如：[29，41]），并在许多关于并发货币的论文中加以利用[16];另见[1]。SOS的大步形式（也称为自然语义[15]）在标准ML的设计过程中使用，并给出了该语言的官方定义[17]。DSOS使用规则来指定转换关系。SOS使用规则来归纳涉及抽象语法树和计算值的状态的转换关系当描述一个纯函数式编程语言（或纯过程演算，如CCS [16]）时，SOS规则看起来非常简单。例如：3E1−→E1Jcond（E1，E2，E3）−→ cond（E1J，E2，E3）（一）cond（true，E2，E3）−→E2（2）3.在说明各种语义框架时，我们将使用一种独立于语言的抽象语法符号。 一般来说，文献中的规范使用的符号强烈暗示了其语义被描述的特定语言的具体语法。风格上的差异没有技术意义。警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4149►−→−→cond（false，E2，E3）−→E3（3）请注意，在上面的SOS规则中，转换上没有标签：标签通常只在与并发进程之间的通信和同步有关的SOS中使用在下一节中，我们将看到标签在SOS框架的模块化变体MSOS中得到了更广泛的利用。D状态不限于语法树。在原始SOS框架中，语法没有与辅助语义实体明确分离：语法和语义实体都被允许作为状态的组成部分，如下面结合绑定和存储所示。相反，MSOS坚持认为，国家仍然是纯粹的句法，我们将看到在节。3 .第三章。2.1绑定声明（和其他一些构造）将标识符绑定到特定的值。绑定映射或环境给出标识符和它们的绑定值之间的当前关联，并且通常具有有限的范围。D绑定通常由状态的显式分量表示事实上，SOS中绑定的处理有些笨拙。假设表达式求值的状态包括绑定：State= Exp× Env。 这需要指定环境ρ保持不变的跃迁（E，ρ）−→（EJ，ρ）。显然，每次指定一个转换时都要写（和读）两次ρ，这将是乏味的，通常的做法是引入符号ρEEJ作为（E，ρ）的缩写（EJ，ρ）。因此，当所描述的函数式语言涉及绑定时，上面给出的SOS规则将被重新表述如下：E1−→E1Jρcond（E1，E2，E3）−→cond（E1J，E2，E3）（四）ρcond（true，E2，E3）−→E2（5）ρcond（false，E2，E3）−→E3（6）50警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41或者，可以在计算完绑定后立即消除绑定，方法是在整个绑定范围内用绑定值替换标识符。然而，要明确定义ρ在T中的代换的结果[ρ]T，需要为每个非约束结构T指定一个冗长的定义方程，例如：[ρ]cond（E1，E2，E3）= cond（[ρ]E1，[ρ]E2，[ρ]E3）（7）以及一些用于绑定结构的相当复杂的方程2.2店不可逆性涉及对存储中特定位置的（不可逆的）更改变量标识符通常绑定到位置，并且赋值会影响存储在位置上的值，但不会影响当前绑定。D绑定和赋值的单独建模允许对别名的最好不要混淆绑定和赋值。抽象地说，变量声明的作用是分配存储区的一部分来保存变量的值，并将标识符绑定到某个实体，传统上称为位置，该实体引用存储区的该部分;它也可以初始化变量的值给变量赋值只会影响存储，而不会影响变量标识符的绑定。这种区别的有用性在允许所谓的别名的语言中表现得最为明显，其中变量标识符被绑定到同一位置：为其中一个变量赋值会导致其他变量的值也发生变化存储器上的D项由状态的显式存储组件表示当所描述的语言不是纯函数式的，并且表达式评估可能有副作用时，表达式评估的状态包括当前存储以及环境：State=Exp×Env×Store。 这种状态之间的跃迁记为ρ <$E，σ −→ EJ，σJ，因此上面给出的规则可以重新表述如下：ρ<$E1， σ−→E1J，σJρcond（E1，E2，E3）， σ−→cond（E1J，E2，E3），σJ（八）ρcond（true，E2，E3），σ−→E2，σ（9）警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4151123123232233ρcond（false，E2，E3），σ−→E3，σ（10）ρ<$E1， σ−→E1J，σJρassign（E1，E2）， σ−→assign（E1J，E2），σJρE2， σ−→E2J，σJρassign（E1，E2）， σ−→ assign（E1，E2J），σJ（十一）（十二）ρn赋值（L，V），σ−→（），σ[L<$→V]（13）2.3通信并发进程之间的通信由转换上的标签表示最后，假设表达式评估可以涉及过程创建和通信。SOS中的传统技术是在这里为转换添加标签。上述SOS规则将重新拟订如下：ρ∈E， σ−L→EJ，σJ11（十四）ρcond（E， E， E）， σ−L→cond（EJ， E， E），σJρcond（true，E，E），σ−τ→ E，σ（15）ρcond（false，E，E），σ−τ→E，σ（16）（τ是一个固定的标签，表示一个沉默的、不交流的步骤。当状态的组成部分或转换上的标签被添加、更改或删除时，规则需要重新制定如上所述，传统SOS中的规则的制定必须在转换中涉及的模型组件（即状态和标签）发生变化时发生变化。这与MSOS的情况形成了鲜明的对比，在MSOS中，规则中的转换的表达是稳定的，允许每个编程结构的规则被定义性地给出，一劳永逸，正如我们将在节中看到3 .第三章。52警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）412.4小步和大步风格在传统的SOS中，小步和大步的风格通常被认为是可供选择的。形式上，大步风格可以被视为小步风格的特殊情况：大步风格的计算还要注意，如果定义了一个小步长SOS，小步长关系的传递闭包提供了相应的大步长关系。在实践中，SOS描述的作者通常选择一种风格或另一种风格，然后坚持下去，因为改变风格涉及重大的重新表述。然而，一般来说，混合使用小步和大步风格似乎更好，通过考虑其计算的性质为每种结构选择更合适的风格：大步长SOS更适合于计算是纯求值的构造，没有副作用，没有异常，并且总是终止-例如，用于将十进制数计算为数字，用于将模式与值进行匹配，以及用于类型;对于所有其他结构，小步长SOS更好，因为它明确了计算步骤的顺序，这通常是重要的。此外，小步骤SOS比大步骤SOS更容易处理指定交叉、异常处理和并发性。DBig-step SOS可以应用于建模语言。有时，建模语言用于指定软件的声明性方面，例如对象类之间的关系重点是模型的静态结构，而不是任何行为解释。虽然小步长SOS不适合于指定静态结构，但只要抽象语法是树结构的，大步长SOS可以在这里用于给出预期语义的形式化描述例如，一个构造和它的计算值之间的大步转换关系可以表示该值满足该构造;一个对象可以被认为满足它所属的任何类CASL中代数规范和代数之间的满足关系是使用big-step SOS [27，Part III]定义的D小步长SOS可以应用于建模语言的行为语义例如，可视化建模语言State-Flow已经通过将图转换为抽象语法树，然后以传统风格定义其小步SOS来指定[8]。警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41532.5非正式公约标准ML的官方定义并不完全正式。纯大步风格的SOS的一个主要例子是标准ML的定义 [17]。描述涵盖了整个语言的静态和动态语义（包括核心和模块级别），并由一组高素质的作者精心编写。然而，其正式程度仍有待改进，特别是在通过的两项“公约”方面“存储约定”允许在规则中隐式地保留存储，而不对其“异常约定”允许省略一些规则，这些规则只是让未处理的例如，考虑以下条件表达式的求值规则ρE1−→真ρE2−→Vρcond（E1，E2，E3）−→V根据上述约定，该规则包含以下三个规则：ρ<$E1，σ−→true，σJρ<$E2，σJ−→V，σJJρcond（E1，E2，E3），σ−→V，σJJ（十七）（十八）ρ∈E1，σ−→raised（EX），σJρcond（E1，E2，E3），σ−→raised（EX），σJ（十九）ρ<$E1，σ−→true，σJρ<$E2，σJ−→ raised（EX），σJJρ<$cond（E1，E2，E3），σ−→raised（EX），σJJ（二十）其中，raised（EX）表示子表达式的计算引发了值为EX的异常。当使用下一节中描述的MSOS方法54警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41112312133模块化SOSD模块化SOS允许一次性描述单个结构正如其名称所暗示的，模块化SOS（MSOS）[22，23，25，26]是SOS的一个变体，它确保了高度的模块化：指定各个语言结构的MSOS的规则可以一次性给出，因为它们的公式化完全独立于所描述的语言中其他结构的存在或不存在当使用并发原语和/或引用扩展纯函数式语言时，函数式构造的MSOS规则在指称语义中，获得良好模块性的问题受到了广泛关注，并且在很大程度上通过引入所谓的monad transformers [18]得到了解决MSOS为操作语义的结构化方法提供了一个类似的（但明显更简单的）解决方案在MSOS中，D状态是纯语法的，并且标签比SOS中更多地被利用MSOS的关键特征是坚持状态仅仅是抽象的同义词和计算值，省略了SOS中包含的通常的辅助信息（如环境和商店）。唯一留给辅助信息的地方是过渡的标签。这个看似微小的符号变化，加上使用符号索引来访问辅助信息，是令人惊讶的有益。许多语言结构的MSOS规则可以独立于标签可能具有的任何组件进行指定;需要特定组件的规则可以访问和设置这些组件，而根本不提及其他组件。控制流的构造规则特别简单。例如，条件表达式的MSOS规则不要求标签具有任何特定的组件，并且它们的公式仍然有效，而不管表达式是否是纯函数式的，是否具有副作用，是否引发异常，或者是否与并发进程交互：E−X→EJ（二十一）cond（E， E， E）−X→cond（EJ， E， E）cond（true，E2，E3）−→E2（22）警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4155121−−−−−−→21122cond（false，E2，E3）−→E3（23）上述第一条规则中的标签X可以包括当前环境、初始和最终存储以及任何发出的通信信号。当标签被省略时，如在第二和第三规则中，要求转换是不可观察的，没有对存储的改变，并且没有发出通信信号。计算中相邻转换上的标签必须是可组合的：绑定必须保持固定，并且转换上标签的最终存储4D在标签中涉及辅助信息的规则仅涉及所需的组件。E−X→EJ（二十四）assign（E， E）−X→ assign（EJ， E）1 21 2E−X→EJ（二十五）assign（E， E）−X→assign（EJ，EJ）σJ=σ[L<$→V]，U∈ Unobs（二十六）assign（L，V）{σ，σJ，U}E在上面的前两个规则中，标签X是任意的。然而，在最后一个规则中，确定了转换开始时的存储σ和转换结束时的存储σJ之间的关系，并且要求任何其他分量是不可观测的。4归约语义这个框架是由Felleisen和他的同事在20世纪80年代末开发的它主要用于理论研究，有时比SOS更受欢迎;例如，Reppy使用Reduction Semantics来定义并发ML [33]。D状态是抽象语法树，对应于格式良好的术语。状态它们纯粹是句法上的。例如，数值表达式计算[4]事实上，标签形成了一个类别。256警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41→J−→→十进制数字而不是抽象的数学数字。但是，如果需要，可以将辅助结构添加到抽象语法中（如SOS中）。D转换是项重写步骤，称为约简。术语重写本身就是一个有趣且发展良好的主题[4]。重写步骤称为归约（无论结果项实际上是否小于前一项）。在约简中被重写的子项称为redex，得到的子项称为reduct。通常可以在任何子项中进行缩减，并继续下去，直到不可能再缩减为止--也许永远不会终止。DRedex仅限于在评估上下文中出现。当被约简的术语对应于程序的抽象语法时，约简的赎回位置应该被限制为遵循计算控制流程（否则可能会在程序的某些部分过早地进行约简，这些部分甚至不应该被执行，导致意外的结果）。评估上下文C：Ctx是具有单个孔的项。如果t是一个项，则C[t]是用t替换C中的洞的结果。在上下文C中的约化记为C[t]−→C[tJ]（用较长的箭头表示），只要有普通约化t t（用较短的箭头表示），就可以进行约化。实际上，这里的C[t]通常是t的整个程序上下文，假设没有进一步的规则允许在某种情况下将减少视为普通减少。也可以给出重写上下文以及该上下文中的项的规则：C[t]CJ [tJ];在这种情况下，t不需要tJ应该是一个普通的 约简。在归约语义中使用的求值上下文由上下文无关语法指定D简单SOS规则对应于还原。将SOS与归约语义相比较，SOS的简单规则一般直接对应于普通归约的规则。例如，考虑以下归约规则，用于在条件表达式的条件已被求值后继续其求值：cond（true，E2，E3）→E2（27）警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4157cond（false，E2，E3）→E3（28）D条件SOS规则对应于求值上下文的产生式许多条件SOS规则只是简单地表达了计算的控制流程，例如指示哪个子表达式首先被计算。这些SOS规则不对应于归约规则，而是对应于用于求值上下文的语法中的产生式。例如，用于评估条件表达式的条件和赋值表达式的两侧的规则对应于以下上下文的产生式：Ctx：：= cond（Ctx，Exp，Exp）|赋值（Ctx，Exp）|赋值（Exp，Ctx）条件表达式的进一步上下文的缺乏防止了分支的过早减少赋值表达式中子表达式的求值顺序在上面是开放的，允许交错;顺序求值将通过使用assign（Val， Ctx）而不是assign（Exp， Ctx）来指定D替换评估上下文的还原不直接对应于SOS规则。归约语义的一个显著优点是，它可以直接指定规则，这些规则可以检查正在评估的子表达式的整个上下文例如，下面的规则清楚地说明了当“exit”被求值时C[exit]−→ null（29）可以用类似的方式指定异常，尽管将异常处理限制在最里面的匹配处理程序需要引入许多新的求值上下文。D计算值只是标准形式的规范项对于ML这样的语言，在归约语义中计算的值不仅包括数字和布尔值，还包括元组、列表和以值为组件的记录。值的语法由上下文无关的语法指定-例如，通过从完整抽象语法的语法中获取表达式Exp的一些结果，并将Exp替换为Val（除非在抽象中）。58警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41D绑定是用替换来表示的，这本身就很繁琐。代换将标识符替换为它们所绑定的值，并且可以由归约规则指定（或等式定义）。不幸的是，在归约语义中，除了使用替换来处理局部声明语义中出现的绑定之外，没有其他选择存储器上的D项通过重写存储项来表示表示存储的项是一系列规范赋值，即位置和值已经被评估的赋值。与本地绑定的情况相反，只有一个存储级别，因此它可以作为整个程序上下文的单独组件保存：ProgCtx：：= Ctx-ctx（Ctx，存储）Store：：= skip |seq（Store，update（Loc，Val））当赋值表达式（或语句）的左右两侧已经求值时，赋值的结果只是简单地添加到存储中，通过给出一个替换整个上下文的- ctx（C[assign（L，V）]，σ）−→- ctx（C[null]， seq（σ，update（L，V）（三十）检查存储在特定位置的值也涉及上下文，但不会更改它：σ= seq（σJ，update（L，V））- ctx（C[stored（L）]，σ）−→σ= seq（σJ，update（LJ，V）），Lj=LJ，- ctx（C[stored（L）]，σJ）−→- ctx（C[stored（L）]，σ）−→（三十一）（三十二）通信的归约规则涉及所涉及的并发过程的单独的评估例如，假设一个并发进程系统被表示为从线程标识符到线程状态的映射，则同步通信警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）4159→可以这样指定申请{I1=C1[send（K，V）]}+{I2=C2[receive（K）]}+TM−→{I1=C1[null]}+{I2=C2[V]}+TM（三十三）5抽象状态机语义抽象状态机（ASM）是一种操作语义框架，由Gurevich在20世纪80年代后期提出其主要目的是在适当的抽象层次上指定计算的各个步骤;控制流程和绑定范围等问题被认为是次要的。该框架已应用于几种主要语言，包括ML和Java。然而，ASM规范的细节和一般风格在不同的出版物之间有很大的差异;在这里，我们将遵循[38]，它似乎在可访问性方面与SOS竞争D状态解释静态和动态函数符号。函数符号的解释是从参数到结果的映射当map在计算过程中不改变时，该函数被称为static相比之下，动态函数在特定参数上的值可以被初始化，更改或定义。没有参数的静态函数对应于普通常量，而没有参数的动态函数对应于简单的可更新变量。例如，对应于算术运算的函数是静态的，给出初始程序抽象语法的无参数函数体相比之下，动态无参数函数pos给出了当前正在执行的短语在树中的位置，表示仍然要执行的内容，其本身由单参数动态函数restbody：PosPhrase表示，其中集合Phrase不仅包含所有可能的抽象语法树，还包含计算值，以及一些节点已被其计算值替换的树。5D转换为特定参数的函数赋值转换可以同时为多个函数的不同参数赋值每个赋值都可能是有条件的，具体取决于值[5]从SOS中熟悉的逐渐用计算值替换短语的想法，最近才被ASM框架采用：在早期的ASM规范中，原始树是静态的，使用单独的动态函数将计算值与树的节点相60警局Mosses/Electronic Notes in Theoretical Computer Science 148（2006）41→表4条件表达式的ASM语义execJ avaExpI=的案例上下文（pos）...cond（αE1，βE1，γE1）→pos：=αcond（）V1，βE2，γE3）→如果V1则pos：=βelsepos：=γcond（αtrue，）V2，γE3）→yieldUp（V2）cond（αfalse，βE2，）V3）→yieldUp（V3）...由函数符号构成的术语。在实际进行任何赋值之前，对同时赋值集合中涉及的所有项进行求值，因此条件的测试和结果状态与赋值的顺序无关。函数在特定参数上的值只会因为显式赋值而改变：它们在其他参数上的值保持稳定。DASM规范经常引入辅助符号。适当的辅助符号的引入允许转换规则被相当简洁地指定。然而，不同语言的ASM规范往往会引入不同的辅助符号，这导致同一构造的规范非常不同，并且很难在另一个ASM中直接重用一个ASM的转换规则。例如，在Java的ASM规范中引入的辅助符号[38]包括：• context（pos），返回restbody（pos）或restbody（up（pos））;• yieldUp （ V ） ， 对 与 pos ： =up （ pos ） 同 时 执 行 的 转 换 restbody ：=restbody[V/up（pos）]进行简化，从而将短语被其计算结果V的替换与pos的调整相结合。为了“简化符号”，位置直接以短语的模式表示，pos的当前值被写为“”。在这些描述之后，可以指定用于评估Java条件表达式的转换规则如表4所示。请注意，转换是由写有'：='的赋值指定的