K工具：编程语言设计的理论与形式化方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记304（2014）57-80www.elsevier.com/locate/entcsTheKPrimer（version 3.3）http://k-framework.orgTraianFlorinS，erbaunut，中国布加勒斯特大学traian. fmi.unibuc.ro安德烈·阿鲁索艾University Alexandru Ioan Cuza of Ias， iandrei. info.uaic.ro大卫·拉扎尔麻省理工lazard@mit.edu查基·埃里森伊利诺伊大学香槟分校celliso2@illinois.edu多雷尔·卢卡努University Alexandru Ioan Cuza of Ias， idlucanu@info.uaic.roGrigoreRos，u伊利诺伊大学香槟分校grosu@illinois.edu摘要本文简要介绍了K工具，一个正式定义编程语言的系统它表明如何顺序或并发语言可以在K中定义简单和模块化。这些形式化的定义会自动产生语言的解释器，以及程序分析工具，如状态空间探索器。关键词：理论与形式化方法，编程语言设计http://dx.doi.org/10.1016/j.entcs.2014.05.0031571-0661/© 2014 Elsevier B. V.保留所有权利。58T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）571介绍编程语言是计算机和运行在计算机上的软件之间的关键联系。虽然编程语言通常有一个正式定义的语法，但它们的语义并非如此语义通常以自然语言的形式给出然而，如果没有一个正式的语言语义，就不可能对该语言的程序进行严格的推理。此外，一种语言的形式语义是一种规范，它为用户和实现者提供了一个坚实的基础，以便在程序的意义上达成一致。当然，为编程语言提供一个完整的形式语义是非常困难的。这部分是因为所涉及的数学，部分是因为糟糕的工具支持，但也因为许多框架的可扩展性差，无论是在定义级别的模块化方面，还是在模拟，执行和/或分析时间方面为了解决编写语言语义的困难，K框架[28]被引入作为一个语义框架，其中可以定义编程语言，演算以及类型系统或形式分析工具。K的目的一般是证明一种编程语言的形式化规范语言可以同时是简单的，表达性的，可分析的和可扩展的。本文作为K工具[13] 3.2版的介绍、教程和参考，它是K框架的一个实现 我们展示了如何使用该工具不仅可以开发模块化的可执行定义，而且还可以通过测试和行为探索轻松地进行语言设计实 验 。K的定义是用机器可读的ASCII写的，K工具接受它作为输入。 为了执行和分析的目的，这些定义被翻译成Maude [3]重写理论。出于可视化和文档记录的目的，定义都很适合于它们的LATEX数学表示。 图4给出了具有输入和输出的简单计算器语言的K定义（ASCII和数学表示）这种语言在第2节中详细描述。除了教学和原型语言（如λ-calculus，System F和Agents），K工具已被用于形式化C [5]，Python [9]，Scheme [21]和OCL [1，29];此外，Java 7，Haskell和JavaScript的定义正在进行中。关于分析工具，K工具已被用于定义类型检查器和类型推断器[6]，目前正在使用基于匹配逻辑的Hoare类断言开发新的程序验证工具[24，25]，基于谓词抽象的模型检查工具[2]以及研究运行时验证技术[26，30]。所有这些定义和分析工具都可以在K工具网站上找到[12]。2第一个K定义在本节中，我们将指导读者使用K工具编写一个简单完成本节后，读者应该能够轻松地编写和键入EXP语言T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5759在图4中，并编译它并将其用作解释器。由于图4中的定义没有使用K的一些更高级的特征，我们将提供几个扩展，每个扩展展示K的一个特征。本文介绍的代码片段突出显示了K工具识别的关键字和使用斜体预先定义的语法类别的排版;K工具为几个流行的文本编辑器提供了类似的语法突出显示功能，包括vi和Emacs。2.1基本成分当开始使用K工具编写K定义时，建议尽可能多地测试定义，从而在开发过程的早期发现问题，因此，我们首先展示如何尽早获得可测试的定义。2.1.1模块K工具提供了用于对语言特性（语法、求值策略、配置和执行规则）进行分组的模块。模块由以下语法定义模块名称>...端模其中是标识模块的名称。模块名通常只使用大写字母和连字符K定义需要至少有一个主模块;然而，通常认为使用两个模块将（程序）语法与语义隔离是一个很好的做法：和-SYNTAX。将语法与定义的其余部分分开可以最大限度地减少程序解析的歧义。要导入模块，需要在模块的头部之后添加至少一个imports NAME>指令。多个模块可以使用相同的imports指令导入，方法是将它们的名称加模块需要在引用其他模块（的一部分）之前显式地导入例如，在使用EXP-SYNTAX模块中声明的语法之前，需要由EXP模块导入EXP-SYNTAX模块模块EXP-SYNTAX结束模块模块EXP导入EXP-SYNTAX端模块2.1.2编辑定义K定义通常存储在扩展名为“.k”的文件中。假设文件exp.k包含上面定义的模块EXP-SYNTAX和EXP要编译此定义（并间接检查其有效性），可以执行以下命令：$ kompile expkompile假定要编译的文件的默认扩展名。此外，默认情况下，要编译的文件名NAME.k假定包含模块，其中60T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57⟨⟩是name的完全大写版本。成功完成后，kompile什么也不打印。你可以使用kompile选项来改变这些默认值;输入kompile--help来获得详细信息。有了基本的框架模块和工具，我们可以开始建立我们的定义，我们将在下面的部分中描述2.1.3评论K工具允许类似C的注释，由' // '引入单行注释和' /*. */此外，K工具可以帮助识字的人通过LATEX-specificcomments（由y' //@ '和 *@ '引入）编程[18]功能我们将在第5节稍后解释这些。2.2语言语法语言的任何形式语义都首先需要一个形式语法。 虽然K解析器可以解析许多非平凡的语言，但它（目前）并不意味着要替代真正的解析器。我们经常称K用这些语言编写的程序可以使用外部解析器进行解析，并转换为KAST（抽象树）用于执行和分析目的（使用krun的2.2.1用户定义语法K是使用熟悉的BNF表示法的一种变体来定义的，端点用引号括起来，非端点以大写字母开头。例如，语法声明：语法Exp：：=Int| Exp“+”Exp[seqstrict]//addition| Exp“*”Exp[seqstrict]//mysql| Exp“/”Exp[seqstrict]//除法|“ read”//从控制台读取整数| “print”“（“Exp“）”[strict]//将评估结果写入控制台| “（“Exp“）”[括号]定义了一个语法范畴Exp，包含内置的整数和表达式上的三个基本算术运算，以及I/O运算。每个生产都可以有一个空格分隔的属性列表，可以在生产结束时在方括号中指定。例如，在最后一个产品中使用的属性括号指定括号仅用于分组原因-它们将从抽象语法树中省略seqstrict和strict是承载语义信息的属性，用于定义相应构造的求值策略例如，声明加法seqstrict仅仅意味着我们希望在计算加法本身之前从左到右计算plus的参数属性的其他用途是帮助解析器进行运算符优先级和分组，或者指示PDFT. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5761⟨⟩生成器如何显示各种构造。我们将在本文后面更详细地讨论这些问题除非另有说明，否则所有后续语法声明都应添加到EXP-SYNTAX模块中。2.2.2内置函数除了预定义的语义类别（计算、列表、集合、包、映射）之外，K工具还提供了许多内置的语法类别/数据库，以及它们的语义操作。这些内置操作的动态演化列表可以在发行版的include/builtins目录中的文件中找到。 目前支持的内置函数包括布尔（Bool）、无界整数（Int）、浮点数 （Float）、字符串（String）和标识符（Id）。对内置类别的操作（例如那些为基本算术运算符提供语义的操作）是用类别的名称后固定的<2.2.3解析程序我们可以通过解析使用该语法编写的程序来测试语法定义。假设文件exp.k包含模块EXP和EXP-SYNTAX，并且EXP导入EXP-SYNTAX。假设还存在EXP程序2avg.exp：print（（read + read）/2）打印从控制台读取的两个数字的平均值假设定义已经使用kompile编译，kast命令可以用来测试程序解析并查看其对应的K抽象语法树。默认情况下，kast需要从包含K定义文件的目录中运行，比如name.k，以及编译后的定义;请使用--help选项查看如何从其他地方调用kast的更多细节。此外，所有未在用户语法中声明的标记都被假定为标识符。KAST仅仅是具有节点（K）标签的树，其或者与句法产生式相关联（例如，作为代币2.3语言语义K工具中的语义学由三部分组成：提供方便地（重新）安排计算的评估策略，给出配置的结构以保持程序状态，以及编写K规则来描述配置之间的转换。2.3.1评价策略：严格求值策略是语法和语义之间的联系，通过指定如何对语言构造的参数比如说，62T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57加法运算符的两个参数必须在计算它们的和之前进行计算，而对于条件运算符' _？_：_ ’, only the first argument should be evaluated,语法Exp：：= Exp“？“Exp“：“Exp [strict（1）]虽然被加数的求值顺序可能无关紧要，但对于顺序复合运算符（例如，‘语法Exp：：= Exp“;” Exp[seqstrict]由于指定求值策略的规则在大多数定义的形式主义中编写起来很繁琐，K工具允许用户用严格性约束来注释语法声明，这些严格尽管严格性约束具有语义意义，但将它们编写为语法的注释会更方便，因为它们通常引用语法声明中的K工具提供了两个严格性属性：strict和seqstrict。每一个可选地接受一个空格分隔的数字列表作为参数，表示构造严格的位置（1是最左边的位置）。例如，上面的注释如果没有提供参数，那么所有的位置都被认为是严格的。strict和seqstrict之间唯一的区别是，后者确保参数按照列表中参数的顺序进行计算，而前者允许非确定性。特别是，如果没有提供参数，seqstrict会强制执行从左到右的顺序来计算所考虑的构造的参数例如，“+”构造函数的seqstrict注释相反，严格注释也会指定两个子表达式都必须求值，但不约束求值策略。K工具区分一个术语类别KResult，用于确定哪些术语是值或结果。例如，下面的语法声明指定整数是EXP语言中的值语法KResult：：=Int与声明语言构造的语法产生式不同，这种声明的位置在EXP模块中，因为它在语义上将整数定义为结果。关于严格性的更高级的细节（包括更广义的评估上下文的概念）以及使用K工具来探索与严格性相关的非确定性将在本文后面讨论2.3.2计算通过计算结构，在K中可以进行评估的排序。计算结构，简称为T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5763···然后K为计算提供了一个可区分的排序K将用户定义的语言语法扩展到计算中是自动完成的，用于使用syntax关键字声明的构造。上一节描述的KResult排序是K的一个子排序。t1at2a atn形式的计算结构的直觉是，列出的任务将按顺序处理。初始计算通常包含原始程序作为其唯一的任务，但规则可以将其修改为任务序列。从严格性注释中生成的规则是这个排序构造器的主要用户;它们通过在构造本身的求值之前对参数的求值进行排序来例如，条件构造的加热规则如下所示：E1：Exp？E2：Exp： E3：Exp => E1 ~>孔？E2： E3在边条件下，E1不是结果。E1：Exp ~>HOLE？E2：Exp： E3：Exp => E1？E2： E3附带条件是E1是这次的结果2.3.3配置，初始配置在K中，运行程序/系统的状态由配置表示。配置被构造为嵌套的、带标签的单元格，其中包含各种基于计算的数据结构。在K工具中，配置单元格使用类似XML的符号表示，单元格的标签作为标记名称，内容位于开始标记和结束标记之间。例如，EXP的配置为：配置 $PGM：K/k><流><在stream=“stdin”>中。列表/in> . List/out>上面的行描述了EXP的初始配置和配置的一般结构，应该包含在EXP模块中（通常在前几行）。configuration声明由configuration关键字引入，由一个标记为k的单元格和一个单元流组成，其中k用于保存运行中的程序（在这里用类型为K的变量$PGM表示），单元流用于保存输入和输出单元格，单元流用于模拟执行程序配置声明中的in和out单元格包含XML属性流，该属性流用于通过交互式I/O增强从定义生成的解释器，并具有当前可能的值stdin和stdout（参见第2.4节）。初始配置中的变量，例如， 它们应该在程序开始执行时初始化（见2.4节）。K工具当前允许的单元格内容类型只有计算和计算的列表/包/集/映射，它们的排序分别为列表、包、集和映射。这些结构的元素是通过注入计算获得的64T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57(of通过构造函数ListItem、BagItem、SetItem和（用ASCII写成“|->' ） 。因为K排序包含所有构建的-在数据库和用户定义的语法中，这允许“ListItem（I：Int）”、“SetItem（5）”和“x”等项|“5”要写。多个项目以空格分隔，例如：'BagItem（4）BagItem（2）'。 这些种类的单位用y'表示. ’‘.List’配置声明是配置抽象过程（稍后在4.1节中描述）的主干，它允许用户只提及每个语义规则中的相关单元格，其余的配置上下文被自动推断。2.3.4规则K规则描述了运行配置如何通过推进计算和潜在地改变状态/环境来演变。在K工具中，语义规则由rule关键字引入。 K规则描述了配置中的项或子项如何以类似于重写规则的方式改变为另一项：任何匹配规则左侧的项都可以被右侧替换。以下规则将在EXP模块中引入。对于不需要匹配配置的多个部分的基本操作，K规则可能只是看起来像重写规则，在规则的顶部只有一个重写例如，加法和乘法的语义可以通过以下方式完成：规则I1：Int+ I2：Int=> I1 +Int I2规则 I1：Int* I2：Int=> I1 *Int I2由于严格性被假设为照顾评估策略，因此K个规则是在假设严格位置已经被评估的情况下编写的（例如，此外，所有规则都可以具有由需要关键字，并且应该是布尔谓词。 以下规则：规则I1：Int/I2：Int=> I1/IntI2要求 I2 =/=Int 0指定只有在分母不为零时才应尝试除法变量是首字母或单词，后面跟着数字或素数，如Foo 2或X变量可以使用冒号后跟排序名称进行排序。 ‘K工具不要求在使用变量的任何地方都键入变量，但每个规则必须至少键入一次有尝试自动推断类型，但我们在这里假设变量是显式类型的。匿名变量在K工具中由下划线它们允许在规则中其他地方没有使用的变量名被省略。例如，以下是计算条件表达式的规则：规则0？ _：E：Exp =>E规则一：Int？E ：Exp：_=> E需要I =/= Int 0T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5765⇒⇒⇒在第一条规则中，如果条件的计算结果为0，则整个表达式的计算结果为第三个参数，而第二个参数（与匿名变量' _ '匹配否则，如果条件的计算结果不是0，则条件表达式的计算结果为第二个参数，第三个参数将被丢弃。在K中，重写是使用我们称为局部重写的扩展。通过将重写动作推入它们的上下文中，K规则可以省略项的部分，否则这些项将在重写规则的两侧重复。在K工具中，这是通过允许多次出现重写符号（在ASCII中写为=>）来完成的，链接由规则（的左侧）更改的匹配上下文的部分及其相应的替换（的右侧），如图所示。执行I/O的两个规则：rulek> print（I：Int）=> I.</k>. . =>ListItem（I）/out>规则 read => I：Int.& lt;/k>ListItem（I）=>/in>例如，打印规则在配置中执行两个更改：（1）打印表达式被其整数参数替换;（2）包含该整数的列表项替换输出单元格中的空列表（即，将其添加到该列表中）。类似地，read规则将输入单元格中的一个元素替换为空列表(i.e.、将其从该列表中删除）并使用其值作为计算单元中读取在K中，配置的部分可以省略和推断，因此，尽可能在规则中给出。这个推理过程称为配置抽象，依赖于指定初始配置的固定结构。例如，这个策略允许上面提到的读取和打印规则忽略流单元格，因为它可以很容易地推断出来。关于配置抽象的更多细节在4.1节中讨论。作为一个额外的快捷符号，K允许省略两端单元格的内容。在K工具中，这通过在单元格的左端或右端附加三个点（省略号）来指定有了这个约定，我们现在就有了打印和读取规则的完整语义：print如果read如果read在计算单元的开始处被发现，则输入列表中的第一个元素被移除，并且其值被用作read的替换。请注意，与严格性注释相对应的规则既用于确保print或read表达式在处于求值位置时最终到达计算的顶部，也用于确保一旦它们被求值，它们的值将被插回相应的上下文。上述技术使K规则变得简单和模块化。通过保持规则的紧凑性和低冗余性，当配置改变或新的构造被添加到语言中66T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）572.4用krun一旦在K工具中编写了语言的K定义并成功编译（使用kompile命令），krun命令就可以用来执行/解释用定义的语言编写的程序。15<联系我们<流><在>.<联系我们.766<联系我们<流><在>.<联系我们.100/0 ~>打印孔<联系我们<流><在>.<联系我们.Fig. 1. 三个EXP程序及其使用krun图1介绍了三个程序及其使用krun工具的运行如第2.3.3节所述，krun工具在初始配置中开始执行程序，变量然后允许规则应用于配置，并且当没有更多规则应用时获得最终配置。例如，执行p1.exp后获得的最终配置在k单元格中包含15，而其他单元格为空。读取和打印指令将检查输入和输出单元格。由于这些单元格使用stream属性进行了注释，因此每当规则需要匹配in单元格中的项时，krun工具都会从标准输入流中请求输入，并将out单元格中输入的任何内容推送到标准输出流。例如，当执行程序2avg.exp时，krun等待用户输入两个数字（示例中用户输入5和7），然后打印它们的算术平均值（6）;然后，打印最终配置最后，p2.exp的执行显示了两件事：可以将输入管道到程序中，以及卡住的最终配置是什么样子。由于除法的规则是由除数不为零的条件保护的，所以在read被替换为0之后，没有规则可以这在计算开始时由术语“100/0”显示3更先进的K定义功能在本节中，我们将介绍EXP语言的几个扩展，并使用它们来实现前一节中没有提到的几个功能$ cat p1.exp$ cat 2avg.exp$ cat p2.exp（3 *（4 + 6））/2打印（（读+读）/2）打印（100 /读）$ krun p1.exp$ krun 2avg.exp$ echo“0”|krun p2.exp5T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57673.1使用功能特性为了使我们的语言更具表达力，让我们从添加λ和μ抽象开始，将其转变为函数式语言。1 要求“../实验k”2需要“modules/substitution.k”4 模块EXP-LAMBDA-SYNTAX5进口EXP-SYNTAX7语法Val：：=Int8|“lambda”Id“。“Exp [活页夹]9语法Exp：：=Val14模块EXP-LAMBDA15进口EXP + EXP-LAMBDA-SYNTAX16进口SUBSTITUTION18语法KResult：：=Val20规则（lambda X：Id.E：Exp）V：Val21=>E[V/X]10|Exp Exp [seqstrict]//应用程序23规则muX：Id.E：Exp11|“mu”Id“。“Exp [活页夹]12端模块24=> E[mu X：Id.E：Exp/X]25端模块图二. exp-lambda.k：使用函数特性3.1.1在文件中拆分定义较大的K定义通常分布在多个文件中，每个文件可能包含多个模块。作为模块上的import命令的一个文件等价物，一个文件可以使用require指令包含到另一个文件中。require会首先在当前目录中查找路径;如果没有找到，它也会在K发行版的include目录中查找。递归地跟踪require依赖关系树。如果一个文件已经通过另一个require命令包含，它将不会被包含两次。3.1.2粘合剂和替代品lambda和mu都是绑定器，将它们的第一个参数绑定到第二个参数中。我们使用内置的替换操作符来为这些构造赋予语义。为了保证替换正确工作（避免变量捕获），这些构造需要用图2的第8行和第11行所示的绑定器注释进行标记。目前，binder注释只能应用于两个参数的产生式，其中第一个必须是标识符。使用K工具SUBSTITUTION模块完全在K工具中定义，利用上面提到的绑定它导出一个构造为了保证按值调用计算策略，在第10行中声明了应用操作符seqstrict。此外，由于所有没有明确提到单元的规则 一个特殊的类别Val 被引入以允许在整数和λ-抽象上进行匹配（图2的第7约束规则不提及发生在计算顶部的单元格68T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57cell还有助于避免μ展开规则的非终止（第23K不承诺仅基于替代的定义。基于环境的定义也很自然;在这种情况下，环境通常只是配置中的另一个细胞3.1.3去糖语法我们可以通过向我们的语言中添加两个流行的函数构造来展示如何在K工具中去除语法中的糖分：let和letrec。语法Exp：：=“let”Id“=” Exp“in” Exp| “letrec”Id Id“=”Exp“in”Exp我们没有直接赋予它们语义，而是使用规则（让X：Id= E1：Exp in E2：Exp）=>（lambda X.E2）E1 [macro]rule（letrec F：IdX：Id= E1：Exp in E2：Exp）=>（设F =μF. λ X.E1 in E2）[macro]let运算符去糖到λ-抽象的应用中，而letrec去糖到绑定μ-抽象的let构造中。 由于在给出语义时它们不 是 A S T 的 一 部 分 ， 因 此 它 们 对 应 的 产 品 不 需 要 作为 绑 定 器 进 行 注 释 。这些宏将在解析时应用于程序;因此语法声明和宏本身都属于EXP-LAMBDA-SYNTAX模块。3.2命令式特征在本节中，我们以向我们的语言添加命令式功能为借口来解释K工具的另一组高级功能3.2.1报表首先，让我们添加一个新的语法类别Stmt（用于语句），并将其替换为语句结束符而不是表达式分隔符。语法Stmt：：= Exp“;”[strict]| StmtStmt由于我们不希望语句计算为值，因此我们将不使用严格性约束来给出它们的语义。相反，我们给出了表达式语句和顺序组合的语义，其中包含以下两个规则：规则V：Val;=>.规则St 1：Stmt St 2：Stmt => St 1 ~> St 2第一个规则丢弃表达式语句的值;第二个规则将语句排序为计算。同样，我们将语法产生式添加到EXP-SYNTAX，将K规则添加到EXP。T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5769--3.2.2语法列表K提供了对通用语法列表的内置支持：List Nonterminal，terminal代表零个或多个非终结符元素的以终结符分隔的列表。要实例化和使用K内置列表，您必须在语法中为每个实例使用（通常是新的）非终结符别名。 例如，我们可以在EXP语言中添加变量声明。下面的第一个产生式定义了逗号分隔的标识符列表的Ids别名，而第二个使用它来引入变量声明：语法Ids：：=List {Id，“，"}语法Stmt：：=“var”Ids“;”这样，var x，y，z;和var ;都是有效的声明。出于语义目的，这些列表当前被解释为cons-lists（即，由头元素后跟尾列表构成的列表因此，当给带有列表参数的构造赋予语义时，我们通常需要区分两种情况：一种是列表至少有一个元素，另一种是列表为空。为了给var赋予语义，我们在配置中添加了两个新的单元格：env，用于保存从变量到位置的映射;store，用于保存从位置到值的映射以下两个规则指定变量声明的语义：rule< k> var（X：Id，Xl：Ids =>Xl）;.& lt;/k> Rho：Map=> Rho[N/X]/env>... . => N|-> 0. lt;/store>需要fresh（N：Int）。rule var .Ids;=>.[结构]第一条规则声明列表中的第一个变量，方法是添加一个从新位置I（由side条件中的fresh谓词指定）到store单元中的0的映射，并更新env单元中变量名称的映射以指向该位置。第二条规则在没有变量需要声明时终止变量声明过程。‘.Ids’ 一般来说，带点的非终结符表示该非终结符的空集合。我们更倾向于将第二条规则结构化，考虑将剩余的空var声明分解为结构化清理，而不是计算步骤（有关规则类型的更多细节，请参见4.3节4并发性和非确定性本节展示了如何定义与并发和未指定相关的不确定性特征（例如，评价的顺序）。此外，还提出了控制非确定性引起的状态爆炸4.1配置抽象假设我们想用并发特性扩展EXP。 添加在存在并发的情况下，env单元的配置需要进一步调整。首先，每个计算单元都需要一个env单元，以避免一个计算隐藏另一个计算的变量。而且每70T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57环境应该与它的计算绑定，以避免使用其他线程这可以通过在k和env单元格之上添加另一个单元格thread来实现，使用multiplicityXML属性来指示thread单元格可以出现多次。多重性可以用来指定一个单元格允许有多少个副本：0或1（“？’),0 or more (‘在此转换后，配置更改如下：配置<线程多样性="*"> $PGM：K/k>. 网站地图<商店>. 地图<流><在stream=“stdin”>中。列表/in> . List/out>线程派生的可能语法和语义是：语法Stmt：：=“spawn”“{”Stmt“}”规则 spawn{St：Stmt}=>。...& lt;/k>< env> Rho：Map（. => . k<> St Rho.& lt;/thread>）在实践中，配置的变化是非常频繁的，通常需要适应新的语言功能。K这对于模块化来说是至关重要的，因为它提供了一种可能性，即当配置改变时，可以以一种不需要重新访问现有规则的方式编写定义实际上，除了spawn规则之外，其他规则（包括上面的变量声明规则）都不需要更改，尽管涉及到新的线程单元。相反，这个单元格是从上面的配置定义中自动推断出来的（并在编译时由K工具添加）。对于我们在3.2.2节中给出的var规则，这意味着k和env单元将被视为同一线程单元的一部分，而不是每个单元都是不同线程的一部分。K工具可以在只有一种正确的方法来完成规则中使用的配置以匹配声明的配置的情况下推断出此上下文。为了更好地理解我们所说的多重性信息在配置抽象过程中很重要，因为它告诉K工具如何完成类似于会合构造的规则语法Exp：：=“rendezvous”Exp[strict]rule rendezvous I：Int => I.& lt;/k>< k>会合I => I.& lt;/k>由于k单元格没有将多重性设置为继续为我们的语言添加命令式功能，我们可以使用上述信息并添加读取和设置内存中变量的规则语法Exp：：=Id规则 X：Id => I.& lt;/k>.X |->L：Int...& lt;/env>... L|-> I：Int.产品介绍语法Exp：：=Id= Exp[strict（2）]规则 X：Id = I：Int => I.</k>.X |->L：Int...& lt;/env>... L|->（_ => I）.&产品介绍注意这些规则如何避免提及线程单元。T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5771当前实现的一个限制是它不允许在初始配置中出现多个同名单元格。这不是配置抽象过程的固有限制，将在K工具的未来实现中 得 到 纠 正 。4.2高级严格性和评估上下文假设在我们的语言中，我们希望能够允许线程共享任何变量，不仅是线程生成语义所共享的变量，还包括一些后来创建的变量。假设两个线程已经共享一个变量，我们可以使用引用来实现这个目标添加引用的语法和语义是：语法Exp：：=““Id规则&X：Id=>L.& lt;/k>.X |->L：Int...</env>语法Exp：：=“*”Exp[strict]规则*L：Int=>I.& lt;/k>... L|-> I：Int.产品介绍以上仅提供对引用的读访问。为了允许写访问，我们还需要更新赋值的语法和语义语法Exp：：= Exp“=” Exp[strict（2）]规则*L：Int=I：Int...& lt;/k>... L|->（_ => I）.&产品介绍然而，这条规则本身并不足够，因为它假设' * '的参数到目前为止，我们使用严格性注释来处理求值顺序，但是在这种情况下不能使用严格性，因为涉及到两个语法产生式（' * '和' _=_ '）而K上下文可以通过推广严格性注释来解决这个问题它们允许用户声明应该评估任意项中的位置K上下文类似于评估上下文[8，16]。例如，下面是上面需要的context*HOLE=_其中HOLE指定首先评估的位置。由于上下文本质上是语义，我们将它们添加到EXP模块中。上下文可以是有条件的，允许对术语的任何变量（包括HOLE）附加条件。比如说，context_ /HOLEcontextHOLE/ I：Int要求I=/=Int 0指定了除法的求值策略，其中必须首先对分母求值，只有在分母的值不为零时才对分子孔本身可以被约束。例如，在面向对象的语言中，上下文漏洞。X：Id需要HOLE=/=Ksuper指定只有当表达式不是“super”时，选择构造左侧的表达式才应该被计算（到对象闭包）72T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）57⇒4.3控制不确定性在编程语言中，不确定性有两个主要来源和计算顺序。在本节中，我们将解释如何使用K工具来探索这两种非确定性行为。4.3.1过渡在理论层次上，K规则被划分为结构规则和计算规则。直观地说，结构规则重新安排了配置，以便可以应用计算规则。因此，结构规则不算作计算步骤。结构化规则的一个规范示例是为严格性约束生成的规则K语义可以被认为是转换系统或Kripke结构的生成器，每个程序一个。只有计算规则在相应的转换系统或Kripke结构中创建步骤或转换。虽然从理论的角度来看是可取的，但允许所有计算规则生成转换在实践中可能会产生大量的交织。此外，大多数这些交织通常是行为等价的。例如，线程计算步骤2+5 7的事实可能与其他线程无关，因此可能不希望将其视为交织空间中的可观察 由于K工具无法知道（没有帮助）哪些转换需要探索，哪些不需要，我们的方法是让用户明确地说，允许将具有某些属性的规则声明为“转换”。在研究程序的转换系统时，只有带有标记为转换的属性的规则才被认为例如，假设我们想要研究由包含程序的EXP程序p5.exp的print语义生成的非确定性print（1）;print（print 2）;打印3要做到这一点，我们可以用print标记注释print规则（以便能够引用它），并使用kompile--transition“print”重新编译。为了包含输出并更好地说明我们的观点，我们考虑将EXP更简单地定义为图1中所示的多线程计算器语言 4;然而，提出的技术扩展到更复杂的语言。图3显示了在p5.exp上使用krun工具的--search4.3.2非确定严格性虽然理论上是好的，但不受限制地使用加热/冷却规则可能会产生巨大的，往往是不可行的大空间的可能性进行分析。因此，出于性能原因，K工具选择一个默认的任意但固定的顺序来评估严格语言结构的参数。具体地说，类似于重新聚焦语义[4]，一旦选择了一个Redex的路径，就不会选择其他路径，直到该路径上的所有Redex都被评估。这具有由于错过的交织而潜在地丢失行为的副作用T. F. Serbanut aetal. /ElectronicNotesinTheoreticalComputerScience304（2014）5773$ krun p5.exp --search搜索结果：<流><在>.<联系我们“一三二”<流><在>.<联系我们“一百二十三”<流><在>.<联系我们“三一二”