模块化语言开发框架及其类型推理算法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记322（2016）119-134www.elsevier.com/locate/entcs模块化语言开发框架Walter Cazzolaa，1 Paola Gianninib，2 Albert Shaqiria，1a米兰大学信息学院b/Piemonte Orientale大学，计算机科学研究所，Disit摘要模块化和组件重用是可以加速领域特定语言的设计和实现的概念。已经开发了几个模块化开发框架，它们依赖于属性在组件之间共享信息。不幸的是，模块化也促进了孤立的开发，并且由于缺乏协调，属性可能会被定义或使用不一致。这项工作提出了1）一个类型系统，允许跟踪属性和静态验证组合对属性缺失或误用; 2）为该类型系统提供了一个正确完整的类型推理算法。 类型系统和推理基于Neverlang开发框架，但也讨论了如何与不同的框架一起使用关键词：模块化和组合，模块化语言实现，组合的形式验证，类型推理1引言领域特定语言（DSL）现在变得越来越重要，但它们的发展仍然很困难，这包含了它们的适当传播。简化DSL开发的一种方法是通过将语言及其实现模块化，最大限度地重用松散耦合的语言组件，其中语言组件是任何面向语言的概念，应该是语言及其实现的一部分根据这种趋势，已经开发了几个模块化开发框架，例如Lisa [9]，JastAdd [5]，Silver [11]，Spoofax [7]和Neverlang[10]。每个语言组件的实现都提供了语言概念本身的语法描述以及支持预期的部分资金由“Progetto MIUR PRIN CINA Prot. 2010LHT4KM”。1 电子邮件：{cazzola，shaqiri}@di.unimi.it2电子邮件：giannini@di.unipmn.ithttp://dx.doi.org/10.1016/j.entcs.2016.03.0091571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。120W. Cazzola等人/理论计算机科学电子笔记322（2016）119语义对于这样一个概念。组合通常由语言组件的语法描述驱动，该语言组件提供与其他语言组件的接口。即使松散耦合，实现不同语言组件的语义的代码也”[8]。作为组合语法驱动的，在开发/组合时很少考虑属性存在的语义约束。模块化开发简化了语言组件的重用，促进了它们的单独开发。语言组件是独立开发的，并依赖于命名约定或类似的经验作为黑盒重用。当语言组件可以单独编译和动态组合时，这可能变得不可靠，如Neverlang，因为它们依赖于不属于组件如果没有一些静态检查，组成可能会变成一个真正的混乱。除了提供语言转换引擎的Spoofax [7]之外，所有其他方法都利用属性语法[8]和语法直接翻译[1]的变体。一个典型的（危险的）情况是，一个语言组件在这种情况下，即使可以完成组合并生成编译器，在使用时也会失败此外，当属性像Lisa [9]中那样声明或像Silver [11]中那样预先计算时，仍然不能保证它们被一致地使用。在这项工作中，我们通过提供一个类型系统，静态验证的组合相对于属性的独立的语言组件实现的属性可追溯性的问题正式化。验证是在Neverlang框架上定制的，但它可以很容易地适应其他模块化语言开发框架，如Lisa和Silver。本文的结构如下。第2节介绍了属性语法中的良好定义问题，如何将其置于Neverlang框架中，并概述了所提出的解决方案。第3节介绍了Neverlangslice的形式化，它在第4节中被用来定义一个小步操作语义，该语义指定了语义动作如何定义、访问和修改语法树的属性。第5节介绍了一个类型系统的类型装饰版本的片，防止运行时错误和状态的可靠性结果。第6节概述了类型推理算法，并指出它对于类型系统是正确和完整的。在第7节中，讨论了一些相关的工作和所提出的系统对它们的应用。第8章得出一些结论2概述属性文法中的良定性。自属性文法诞生以来，确保文法定义良好的问题就已经得到了解决在纯属性语法的上下文中，良定性传统上是W. Cazzola等人/理论计算机科学电子笔记322（2016）119121模块IfThenElse {引用语法{}public void run（）{IF：ExpD“if” Exp“then” Exp“else” Exp;如果：{$IF[1];if（$IF[1].val））{$IF[2];$IF.val =$IF[2].val;}否则{$IF[3].val =$IF[3].val;}}.}}模块编号{引用语法{}public void run（）{DBL：Exp D/\d+\.\d+/INT：实验D/\d+/INT：.{$INT.val =new String（#0.text）;}.DBL：。{$DBL.value =new Double（#0.text）;}.}}以封闭性和非圆性表示。闭包属性声明每个属性都有一个计算其值的语义规则。纯属性文法总是将属性值与没有副作用的函数相关联;通过函数的定义，这总是赋予属性定义。在这种情况下，闭包属性的检查只包括验证函数的定义。不幸的是，许多工具并不采用完全定义的属性语法，尽管存在规则，但它可能不设置属性。在这些工具中，我们发现了Yacc，ANTLR，Silver[11]，Neverlang [10]和Lisa [9]。非循环属性声明属性值不能依赖于属性本身。 在作为一个整体的设置，Knuth [8]提出了一个算法，用于测试文法的闭包和非循环性。 Vogt等 [12]在高阶属性文法的上下文中扩展了Knuth算法。Backhouse [2]提出了一个包含闭包和循环性检查的定义性测试。虽然不是微不足道的，但与在模块化模型上进行的相同分析相比，整体方法中的良好定义性分析很简单，就像我们的模型一样，信息隐藏引入了有趣的挑战。在这样的背景下，Kaminski等人 [6]提出了一个适用于模块化系统的属性文法的良好定义性分析。分析检查主机语言及其扩展的组合导致一个完整的语法定义，在属性方程中没有循环依赖关系。建议的解决方案被应用到银，属性文法系统支持通过转发扩展永不言弃Neverlang是一个用于组合语言开发的框架。Neverlang的功能的完整阐述在下文中，我们仅描述这项工作中所需的那些特征Neverlang的基本单元是实现语言特性的切片[10]。切片通过一些语法规则定义自己的语法它还定义了语义角色，即，与语法规则相关联的一组语义动作角色表示单树遍历，并且在遍历期间执行语义动作。语义动作是用类似Java的DSL编写的，它允许定义和使用属性。角色可以在切片收集和/或重用的模块中定义。清单1：if-then-else实现。清单2：Numbers实现。清单1显示了一个实现if-then-else构造函数版本的模块。reference语法通过单个产生式定义if表达式语法。按照惯例，非终结符要大写，而终结符要括起来122W. Cazzola等人/理论计算机科学电子笔记322（2016）119用引号。每次生产之前都可以有标签（例如，可以在语义操作中使用的，以引用产生式非终结符。在我们的示例评估中，每个角色都与一个名称相关联。语义动作写在中间。{和}。符号.一个动作通过一个先于其定义的标签与其生产相关联。清单1中的示例有一个与语法中唯一的产生式关联的语义操作。给定一组模块，Neverlang为实现的语言构建一个基于树的解释器/编译器。对于一个给定的输入程序，解释器将构造它的语法树，并按照一个单独的配置文件中指定的顺序为每个角色遍历它。每当访问节点n时，运行时系统将执行与用于构建以n.在我们的示例中，每当访问表示头非终结符Exp的节点时，都会执行标记为IF的操作。在遍历过程中，树可以用动态附加到树节点的任意属性语义动作代码可以通过使用以下语法$label[offset]引用关联生产的所有非终结符，其中label是标识关联生产的标签头部非终结符的o值设置为0。所以在上面的例子中，头非终结符可以用$IF[0]或简单的$IF来引用。表示if-then-else表达式的条件部分的第二个非终结符可以由$IF[1]引用，依此类推。语 义 动 作 首 先 遍 历 表 示 if-then-else 构 造 的 条 件 部 分 的 子 树（eval$IF[1]）。这种遍历可以在由$IF[1]表示的节点中定义新的属性。这些属性可能来自实现Exp非终结符的其他模块。根据$IF[1].val属性的值，我们继续遍历if-then-else构造的一个分支（eval$IF[2]或eval$IF[3]）。在这两个分支中，我们将分支的val属性复制到当前节点。问题陈述。由于Neverlang中属性的性质是动态的，因此在需要时可能不会定义属性。基本上有两个原因。首先，只有当遵循特定的计算路径时，属性才可能被定义。例如，让我们假设清单1中的else分支遗漏了$IF.val = $IF[3].val;语句。在这种情况下，在语义动作执行结束时，属性$IF.val可能不会被定义。另一方面，由于不同的命名约定或仅仅是分散注意力，具有相同目标的属性可能在不同的模块/语义动作中被标记为不同的名称让我们考虑清单2，其中定义了整数和浮点数。这两个规则分别定义正则表达式匹配整数和双精度。因此，当解析器匹配一个数字时，它将构建一个以Exp为根的子树，子树中包含匹配的值。语义操作只是提取匹配的数字（由词法分析器存储在#0.text中）并将其值放入属性中。double-labeled byDBL-的语义动作定义了一个名为value而不是val的属性。因此，语言不能保证Exp非终结符总是具有val或value属性。当编写由不同团队开发的实现的编程特性时，W. Cazzola等人/理论计算机科学电子笔记322（2016）119123解决方案概述。 为了识别这些错误的情况，Neverlang的形式化描述了框架中涉及的所有相关实体及其形式语义。为了防止错误，我们引入了Neverlang的一个装饰用于评估结果：如果语义动作的代码相对于这些装饰是良好类型的，则对语言的任何字符串的语法树的计算正确地进行。结果假设我们有一个完整的语言实现，然而，由于开发是组合的，我们通过将切片中出现的非终结符的定义/使用属性的信息与切片相关联来增量地指定类型检查。为了类型检查切片的组合，我们使用这些信息，即，不需要切片的语义动作的代码回到我们的例子，清单1中的切片是类型良好的，与这个切片关联的类型表明，非终结符Exp要求在与Exp的产生式关联的任何语义操作求值之后定义属性val（因为在eval$IF[1]之后，if条件需要属性val此外，这个切片的所有语义动作（在本例中只有一个）都定义了Exp的属性val。如果情况不是这样，例如，条件的两个分支之一没有定义头部非终结符的属性val清单2的切片也是类型良好的，与此切片关联的类型指定非终结符Exp不需要定义任何属性，切片的语义操作不为Exp定义任何属性。但是，这两个切片的组合并不正确，因为清单2中的切片没有为Exp定义属性val，而另一个切片的类型需要这个属性。如果我们在语义操作DBL中用val替换value，那么清单2中切片的类型将指定属性val是为Exp定义的，并且组合将是正确的。在这种情况下，组合的类型将等于清单1的类型。类型检查所需的类型修饰可以推断出来。在第6节中，我们概述了一个算法，给定一个Neverlang切片，该算法分析其语义动作的代码，并生成与切片相关的非终结符的属性的定义/使用信息。 如果切片不能以类型检查成功的方式进行修饰，则算法失败。此外，如果算法从产生的信息中成功，我们可以导出切片的所有可能的装饰。切片组成的类型推断依赖于此信息，使推断组合。3Neverlang的语法形式化在本节中，我们将介绍Neverlang语法的形式化。考虑了Neverlang框架的一些限制。切片是被考虑的模块化单元。切片只提供一个角色。这些简化并不代表真正的限制。在Neverlang中，语义操作是通过向完整的Java添加用于访问、定义和更新的“域特定”结构来指定的。124W. Cazzola等人/理论计算机科学电子笔记322（2016）119| |→··· ≥{|}属性，并用于强制访问语法树的节点的子树。为了专注于属性操作，我们选择将非“领域特定”的构造限制切片由语法的一部分组成，即，一组产品和一个角色定义。现在我们正式描述切片语法。我们把我们定义的语言称为目标语言。制作和语法。通常，一个文法是一个四元组（n，N，S，n），其中n是终结符的集合，N是非终结符的集合，S是起始非终结符，而n是产生式的集合。 对于我们的目的，终端符号是无用的，所以它们将不包括在切片形式化中。一个产生式是一对非终结子和一个非终结子序列，记为X0X1Xq，其中q0。的空序列由k表示。我们使用带有下标和上标的元变量X来对非终结符进行范围调整此外，我们用P表示文法的产生式的子集（不一定是全部）。生产是唯一标识的标签，p，与下标或上标，如果需要。定义3.1设p是X0→X1···Xq的标号，(i) p[i]，其中i=0，...，q表示Xi，其中i表示产生式p中的非终结位置，p[0]表示产生式的左侧非终结位置(ii) P=q(iii) NT（p，i）=Xi，对于i= 0，.，q和(iv) NT（p）=n0≤i≤q{NT（p，i）}。定义3.2给定一个生产序列P= p1. pm，(i) LP是P中产生式的标签集合，(ii) NT（P）=NT1≤k≤mNT（pk）是P中的非终结符的集合，(iii) Def（P）=N1≤k≤m{NT（pk，0）}是定义在P中的非终结符的集合，(iv) PTX=pkNT（pk，0）=X是P的一个子集，它的乘积有X有左侧非终结符。下面我们给出一个文法的定义，它比标准文法的限制性稍强定义3.3[语法]一个产生式序列P是一个语法，如果NT（P）=Def（P），并且有一个只出现在产生式左边的开始非终结符，我们称之为开始产生式。我们用G表示文法。语义动作的切片和语言。正如在第2节末尾所提到的，切片被形式化为单个角色和每个产品的动作。动作是由以下语法定义的语言的语句。s：：=单位|如果e那么s else s |s; s |p[i].a = e |eval p[i]e ：：=v|p[i].a |op（e 1，.，en）v：：=tr|FLS |nve：：= unit|v语句可以是空语句单元、条件语句、语句序列、表达式、属性更新和/或定义、p[i].a=e或执行W. Cazzola等人/理论计算机科学电子笔记322（2016）119125GG对于语义动作，evalp[i]，其中p[i]指定产生式中位置i处的非终结符，标记为 pinP 。 表 达 式 可 以 是 整 数 或 布 尔 常 量 ， 非 终 结 符 实 例 的 属 性 值（p[i].a），或某些运算符对表达式的应用在示例中，我们将使用+和==。值是表达式计算的结果，可以分配给属性。扩展的值包括unit，它是执行语句的结果，因此也是执行动作的结果。定义3.4[切片和切片组成]• 给定一个产生式序列P，P上的切片SP是由P中的产生式标记的一组动作，由{p：. {s}。| p ∈ P }.• 设P和PJ中的产生式的标号是不相交的。 切片的组成SP和SP′，SP<$SP′，表示P PJ上的切片，SP<$SP′。在切片的定义中，P中的所有产生式都与一个动作相关联的假设并不是一个限制，因为我们总是可以将空语句单元与一个产生式相关联。切片的组合是关联的和可交换的，因为在一个切片中产生式和相应的语义动作可以被重新标记，我们总是可以定义两个切片的组合。4操作语义语义动作的语义以“小步”的风格来指定在操作语义的形式化中，我们指的是产生式序列上的一个切片，它指定了一个完整的语法，如Def中所定义的3.3（它可能是目标语言的子语言尽管一个语言实现可以由一些切片的组合来定义，但根据定义3.4，我们知道这等价于一个包含组成切片的语义动作的联合的单个切片。在语义动作的评估过程中，语法树的结构是固定的，而与其节点相关联的属性是变化的。属性与语法树是分开的。语法树和属性。语法树的定义形式化了目标语言中解析字符串所产生的数据结构。 任何子树一个语法树的子树与一个产生式p相关联，并包含由p右边的非终结符生成的字符串。如果p在右边有一个空的非终结符序列，则节点是叶子节点。唯一标识符与语法树的子树相关联。设I是一个可数的标识符集合，其中id是一个在I的元素上变化的元变量。定义4.1[语法树]设G是一个文法。• 如果p：X0→ X1···Xq∈ G且ηi1≤i ≤q <$PJ：Xi→···∈G使得ηi是pj的语法树，则η_id：（p，η 1 ··· η q）是产生式p的语法树.126W. Cazzola等人/理论计算机科学电子笔记322（2016）119·∃···D• η是G的一个字符串的语法树，记为G|=η，如果η是G的起始产生式的语法树，且η中的所有id s是不同的.• 给定语法树η，η（id）=ηJ，如果p，η1，...，使得ηJ=id：（p，η1ηq）出现在η中。 如果id不发生在η中，η（id）是未定义的。·η的域，dom（η）={id|（i）定义为，例4.2让我们考虑清单1中的IF、INT和DBL结果，2加开始产生式S：S Exp;（S是开始符号），它被添加到变换根据定义3.3将产生式转换成文法。定义包含清单1和清单2中指定的动作的切片，加上动作：史：{eval$S[1]; $S[0].val=$S[1].val;}。输入字符串“if 1 then 2 else 3”的语法树η将是：id1：（S，id2：（IF，id3：（INT，N）id4：（INT，N）id5：（INT， N）所以dom（η）={id i|1 ≤ i ≤ 5}，η（id 1）= η和η（id 3）= id 3：（INT，INT）。映射用于将属性与语法树的节点相地图，m是从集合B到C的具有有限域的部分函数我们写入m=[b1c1，...，Bncn]和m（bi）= ci. 空映射表示为[]。 Ifm=[b1<$→c1， . . bn→<$cn]m的域，do m（m）={b1， .. . ，bn}。的映射m[bJ<$→cJ]使得m[bJcJ]（bJ）=cJ且对于b bJ，m[bJ<$→cJ]（bJ）=m（b）。定义4.3[属性存储]给定一个语法树η，为了表示与η的节点相关联的属性的值，我们定义属性存储，用μ表示，它是从I到A到值的映射，使得dom（η）=dom（μ）。考虑例4.2的语法树η。 属性存储[id1[val›→2]，id2<$$> →[val<$→2]，id3<$$> →[val <$→1]，id4<$→[val <$→2]，id5[ ]]表示，对于与构造（id3）的条件相关联的节点，属性val被定义并且具有值1。对于与开始符号（id1）、if构造（id2）和then条件（id4）相关联的节点，属性val被定义为值2。对于与else条件相关联的节点id5此属性存储区是对与生产S以属性存储开始，其中所有节点都没有定义的属性。请注意，对于id5，属性val没有定义，因为toBool（1）为true，所以节点id5不会被评估。运行时术语和配置。为了定义语义动作的语言的小步执行，我们需要参考：（通用）语法树η，与η相关的属性存储，给出当前为η定义的属性（及其值）和当前评估的术语t评估的一个步骤产生新的项并且可以修改属性存储μ。我们将约化关系的判断定义如下：η|= t |μ → tJ|μJW. Cazzola等人/理论计算机科学电子笔记322（2016）119127我们把语法树η放在|=因为它在评估期间不会改变。128W. Cazzola等人/理论计算机科学电子笔记322（2016）119˜|η|= op（v）|μ → v |μif oη |=if trthen s else s ′|μ → s |μ（E-IFTRUE）˜p（v）=v（E-OP）˜η |=单位; s |μ → s |μ（E-SEQ）η|= if fls then s else s ′|μ → s ′|μ（E-η|= id.a|μ → μ（id）（a）|μ（E-GETA）η |= id.a=v |μ →单位|μ [id <$→ μ（id）[a <$→v]]（E-SETA）η（id）=id：（p，id1：（· ··）· ·id|p|：（· ··））p：{s}。 ∈SGs′=（s[p[0]：=id]）[p[i]：=idi]1≤i≤|p|（英-英η|= eval id |μ →s ′|μη|= e |μ → e ′|μ ′VAL）η|= op（v，e，e）|μ → op（v，e ′，e）|μ ′(EC-O（P）η|= s 1|μ → s ′1 |μ ′η|=s1;s2|μ→s′1;s2|μ′(EC-SEQ）η|= e |μ →e ′|μ ′η|= if e then s 1else s 2|μ → if e ′then s 1else s(EC-IF）的η|= e |μ → e ′|μ ′η|= id.a = e |μ → id.a =e ′|μ ′(EC-SETA）图1：操作语义规则。运行时配置是由t μ表示的术语和属性存储对，但为了理解μ，我们还需要参考规范η。在语义动作语言中，语法树的节点被引用在productions（p[i]）中使用非终结符实例的标签。在运行时配置中，这些标签被它们所表示的节点的标识符所替代（给定当前操作执行的节点）。运行时术语（即，运行时配置中的术语）被定义为通过用id.a替换p[i].a，用id.a=e替换p[i].a=e，用evalid替换evalp[i]来为语义动作重写语言。操作语义的规则图中给出的操作语义的规则。 1，指定语言的构造的执行如何使用/修改运行时配置。在规则（E-Op）中，v表示整数或布尔值分别对应于语言的数字或tr和fls标记，类似地，op表示与语言的符号op对应的函数。有趣的规则是那些处理属性的规则。Rule（E-G E tA）返回id的属性a的值。如果a不是为id定义的，则该术语是“卡住”的。 规则（E-S E tA）通过将属性a定义为v（或覆盖属性a的值）来修改属性存储μ。求值是一个语句，返回单位。最后，rule（E-Eval）将eval id替换为与生产p相关联的操作，生成id节点。 在动作中，非终结符p[i]的实例被对应于子节点i的标识符所替代，p[0]被id所替代。这将开始访问与id对应的节点。最后四条规则指定了求值顺序，这是命令式/函数式编程语言的标准求值。设id r是η的根节点，且η（id r）=（pr，id 1···id |pr|）. S G中η值的初始配置为|其中：sin=（sr[pr[0]：= id]）[pr[i]：= id i]1≤i≤|pr| 且μin=[id j→ []]1≤j≤n例如，前。4.2，设μin=[idj→[]]1≤j≤5，则初始配置为：evalid 2; id 1. val= id 2. Val|μinW. Cazzola等人/理论计算机科学电子笔记322（2016）119129A{}∈| |∈A}{1}|∈ }.应用规则（EC-SE q）和（E-Eval），我们得到：η|= eval id 2; id 1. val= id 2. Val|μin→ sJ; id 1。val= id 2. Val|μin其中sJ是与清单1中IF标记的生产相关联的操作，如果[i]被idi+2替换，其中i=1，. 3.第三章。5类型系统本节介绍一个类型系统，它跟踪属性定义并防止访问语法树节点的未定义属性。 为了做到这一点，我们假设动作被修饰了两个属性集，一个是产生式左边的非终结符正确执行所需的属性集，另一个是动作执行后将为同一个非终结符定义的属性集。设=a是一组具有固定类型的属性。 这种限制允许关注属性的“定义性”，而不是它们的有效类型，这是一个具有大量解决方案的正交问题。Ta表示属性a的类型。定义5.1类型化切片TSP是一组修饰动作，由P中的产生式{p：（R，D）}标记。{s}。| p ∈ P ∧ R, D ⊆ A}.给定一个p：（R，D）。{s}。 ∈ TSP• R称为所需属性集，是非终结符p[0]，确保s的正确执行，以及• D，被称为属性的定义集，是通过执行s确定为p[0]定义的属性集。对于语义动作的类型检查，通过属性上下文跟踪属性的定义性。定义5.2[属性上下文] p的属性上下文是p中的非终结符对及其属性的子集。 也就是说，{（p[i]，a）|0≤i≤p a给定n，定义n（p[i]）=a（p[i]，a）n。我们说，如果是p的属性上下文，则指代p。在非终结符环境中收集关于执行与P中的非终结符的产生相关联的语义动作所需/定义的属性的信息对于一个产生集P，一个非终结环境Γ是一个集{X1：（R1，D1），.， Xn：（Rn，Dn）|Xi∈ NT（P）<$Ri，Di<$A（1 ≤ i ≤ n）}.我们假设所有的非终结符Xi都是不同的。如果X：（R，D）Γ，则与定义非终结符X的产生式相关联的任何语义动作的执行依赖于与R中的某些属性的X相关联的节点的定义。另一方面，执行这些语义动作中的任何一个都将确保在最后至少定义D中的所有属性。130W. Cazzola等人/理论计算机科学电子笔记322（2016）119►/给定一个非终结符集合M：Γ−M={X：（R，D）|X：（R，D）∈ Γ<$X/∈M}，r T M ={X：（R，D）|X：（R，D）∈ Γ<$X ∈ M}.考虑的基本类型是：T =单位|Int|BoolUnit是语句类型，而Int和Bool是表达式类型。表示语义动作的项t的类型判断是r;pt：T;J其中，Γ是一个非终结符环境，和J是属性上下文，T是一个类型。这个判断应该读作：在非终结符环境Γ和属性上下文中，项t具有类型T，它的求值定义了p的非终结符出现的属性符合J。这个判断是相对于产生式p的，因为我们必须检查非终结符实例的正确性。为了一致性，我们对语句和表达式使用相同的判断，即使表达式总是具有veJ=，因为它们的求值可能不定义属性。图1给出了判断Γ; pt：T;J的类型规则。二、 规则（T-S UB）是对必需属性和已定义属性的标准弱化。 它说，如果从一个属性的文本中我们推导出t是正确的，那么我们也可以推导出一个更大的属性上下文的结果。另一方面，我们推导出，如果t的执行定义了文本中的属性cn_text_n_J1中的属性，则它的执行也定义了cn_J1的子集。表达式的规则（不包括对属性的访问）是显而易见的。规则（T-S E q）说，对于一个语句序列s1;s2，由执行s1定义的属性在执行s2期间可用。 因为s1和s2都必须是语句，所以它们的类型必须是Unit。对于条件语句rule（T-If），条件是一个布尔表达式，两个分支都是语句，所以它们必须具有Unit类型，并且它们必须定义相同的属性集。这不是一个限制，因为使用规则（T-SUB），我们可以削弱属性上下文，使它们相等。 为了正确访问非终结符实例p[i]的属性a，规则（T-G E tAtt），属性上下文必须包含对（p[i]，a）。只有当在当前表达式的求值之前执行与p相关联的动作的语句时，才能为i= 0定义a。 当i = 0时，该属性可能已经在与p相关联的动作的所需属性集中，即，在执行操作之前，它已被定义为p[0]。在规则（T-G EtAtt）中，表达式的类型必须等于它所赋给的属性的类型。因为这些是陈述，它们的类型是单位，它们定义了p[i]的属性a。最后，为了检查evalp[i]，我们必须引用非终结符环境Γ。 设X = NT（p[i]）和Γ（X）=（R，D），R中的属性必须在执行与定义X的产生式相关联的语义动作之前定义。 由于eval p[i]将导致执行这样的动作之一，因此R中的属性必须为p[i]定义。D中的属性是通过执行与定义X的产生式相关联的语义动作来为头部非终结符定义的，因此在执行eval p[i]之后，D中的属性将为p[i]定义。W. Cazzola等人/理论计算机科学电子笔记322（2016）119131∈TS∈ − TS∈TS TSr;{（p [0]，a）|a ∈ R}ps：单位;（T-ACT）rps：（R，（p[0]））rR<$rD<$pksk：（Rk，Dk）（1≤k≤m）do m（rR）=dom m（rD）=domΓD={X：（pk∈（P<$X）Rk，pk∈（P<$X）Dk）|X∈Def（P）}rRTSP={p 1：（R1，D1）. {s1}。， . . . ，pm：（Rm，(T-S虱子）（ΓR<$ΓD）−Def（P）<$TSP：ΓDTDef（ P）（ΓR<$ΓD）−Def（ P′）<$TSP'：ΓDTDef（ P′）<$R<$TSP<$TSP'：ΓD（T- OMP）Ψ′⊆Ψ′1Ψ1⊆ΨΓ;1pt：T;′1（T-SUB）T;T′Γ;ptr/fls：Bool;（T-TR/FLS）Γ;punit：Unit;（T-UNIT）Γ;pn：Int;（T-INT）r; n=pe：T; n= ptype（op）=（T，T）（T-OP）r;pop（e）：T;Γ;布尔值e：布尔;布尔Γ;ps：单位;′Γ; ps′：单位;′（T-IF）Γ;pifethenselses′：Unit;′Ta; Tb; T a ;T b; T a ; T b; T 0≤i≤|p|（T-SETATT）r; pp[i].a=e：Unit;{（p[i]，a）}Γ;ps：单位;1Γ;1ps′：单位;2（T-SEQ）Γ;ps;s′：单位;12（p[i]，a）∈φ0≤i≤|p|（ T-GETATT）r; pp [i].a：Ta;NT（p[i]）：（R，D）∈ΓR（p[i]）（T-EVAL）r;n =peval p[i]：Unit;{（p[i]，a）|a ∈ D}图2：术语的类型系统的规则图3：良好类型的语义动作，切片和切片复合。图3显示了语义操作和类型化切片的类型化 规则（T-Act）说，一个动作在非终结符环境Γ中有正确的修饰（R，D），如果从Γ和属性上下文中，非终结符实例p[0]具有R中的所有属性，动作的执行为p[0]定义了最终属性上下文中为p [0]定义的所有属性。 在输入切片规则（T-Sl ICE）时，我们区分两个不相交的非终结符集，定义的非终结符XDef（P）和重新定义的非终结符sXNT（P）定义（P）。切片如果在P中定义的定义域不包含对n个终端的假设，且片中的所有动作在非终端环境ΓR，ΓD 中具有正确的装饰 ， 则P是来自于 ΓR的p∈ΓD，其中ΓD不包含n个终端XDef（P），其属性集与定义切片中X的产生式相关联的所有语义动作兼容。也就是说，它要求任何动作所需的属性集的并集，并确保动作所定义的属性集的交集 规则（T-Comp）是指切片的组成P和P′有来自非终结元环r R的yperD，如果P可以从对在P中定义的非终结点的限制中导出，而非终结点由在P中没有定义的非终结点的假设下推广的非终结点矩阵ΓR导出. 对于TSP′也是如此。这确保了在输入TSP和TSP′的动作时对非终结符的假设是一致的。要求完全相同的假设不是一个132W. Cazzola等人/理论计算机科学电子笔记322（2016）119► TS TSTS···TSTS≤≤TS···TS TS−SS⊥限制，因为我们对动作的类型有子类型。我们可以证明，如果PJJ是乘积序列PPj，则ΓR<$TSP<$TSP′：ΓD当且仅当ΓRP′′：ΓD，其中P′′=PP′。 注意，根据定义3.4的合成，P和P j中的产生式的标号是不相交的。最后我们说切片的组成，1n，其中i（1我n）是与产品Pi相关联的切片，是一个良好类型的语言实现，当P1. Pn是一个以pr为起始产 生 式 的 文 法 ， 对 于 某 些 Γ和 D ， 我 们证明了 ： NTS1≠. NTSn ： Γ 和 Γ （ NT（pr[0]））=（T，D）.健全。考虑一个文法G=P1. Pn与一种类型良好的语言实现1附图标记 我们知道这片G=1≤i≤ ni还一个类型良好的语言实现。设η是从文法G导出的语法树，即， G|=η。 健全是由西奥说。 5.3Wheresin|μin是第4节中定义的TS G中η的初始组态。定理5.3（可靠性）如果η |=sin|μin→μs|μ，则s=单位或η |= s |μ → s J|μ J对于一些sJ和μJ。此外，我们可以证明语法树是正确的装饰属性符合类型系统。6类型推断在本节中，我们给出了切片类型推断函数TS的非正式定义，描述了该函数返回的约束，并展示了如何检查约束的一致性和组合。然后，我们陈述了关于类型推理的正确性和完备性的结果。第5节的类型系统。类型推理由一个从切片P到切片中使用但未定义的非终结符的要求NT（P）Def（P）的部分函数TS定义，而P中定义的非终结符的属性通过分析切片的相关语义动作而函数TS是根据局部函数Ta定义的，该局部函数T a对与切片的产生相关联的动作进行分析。切片TS的类型推断函数TS（P）=γ，Γ其中：• γ 是一个包含对非终结符X 的约束的集合，使得X∈ NT （P ）-Def（P），由切片的动作导出。特别地，γ是非终结符和三元组之间的关联集合，记为X：（A1，A2，A），其前两个组成部分是属性集合，第三个组成部分是属性集合或表示集合未定义。 A1和A2中的属性是对定义这些非终结符的切片的要求。也就是说，A1中的属性必须在与定义X的产生式相关联的所需动作集合中;A2中的属性必须在与定义X的产生式相关联的动作的定义集合中。·A中的属性是在SP的动作中定义的属性，··W. Cazzola等人/理论计算机科学电子笔记322（2016）119133- - -→···联系我们S2⊥XXXYYY计算非终结符X的实例的eval。如果没有eval的非终结符X的实例，则A=• Γ在y pe系统中具有Γ D的含义，即， 将非终端X∈Def（P）与它们的所需属性和所提供属性相关联，这些属性是通过对SP的动作分析得到的.TS是根据动作T a的类型推理函数定义的，它将语句s和相关的产生式p作为输入：XX1Xq，如果有定义，使得Ta（s，p）=γ，（R，D）。集合γ具有与T S相同的含义，即，NT（p）X上的约束。集合R和D是X从动作s导出的必需和定义的属性。我们现在通过一个简单的例子来展示如何执行切片组合的类型推断。 设P包含单个产生式pX：X → XY，设P J包含单个产生式pY：Y→XY。因此，NT（P）=NT（PJ）={X，Y}，Def（P）=X并且Def（P）=Y。考虑包含相应产生式的语义动作的切片P和P′。假设• TS（SP）={Y：（AY，AY，AY）}，{X：（RX，DX）}和1 2⊥• TS（SP′）={X：（AX，AX，AX）}，{Y：（RY，DY）}.1 2⊥由类型推断生成的关于两个给定切片的约束必须是一致，以便两个切片可以组合。也就是说，通过其在SP，Y：（AY，AY，AY）中的使用而对非终结符Y作出的要求和通过其在S P，Y：（A Y，A Y，A Y）中的使用而对非终结符Y提供的要求是相同的。1 2 2 3 4 5 6 7 8 9 910 10 11 12 13 1415 16 17 18 19 19中与产生式pY相关联的语义动作P′，Y：（R约束一致，如果得双曲余切值.）. 这些• 操作中非终结符Y的实例所需的所有属性与X相关联的是由与Y相关联的动作定义的，即，AYDY，并且• 如果在关联到的动作中有非终结符Y的实例的eval，X，即AY/= Y，则Y所需的所有属性都由关联的操作Y是在与X相关的动作中的值之前定义的，即 RYAY.(This也应该对X成立，即，对SP′中X的要求必须由与SP中的产生式pX相关联的语义动作来满足。）如果TS（SP）和TS（SP′）返回的约束条件是一致的，则TS