属性文法验证：利用 O-货架形式化方法 确认属性规范性

理论计算机科学电子笔记110（2004）33-54www.elsevier.com/locate/entcs利用O-货架形式化方法验证属性文法性质安东尼·斯隆麦考瑞大学计算机系澳大利亚悉尼，NSW 2109摘要属性文法是许多自动生成编程语言实现的工具的专用语言。我们考虑属性语法规范的属性验证问题，特别是现有工具不支持的属性。而不是提出扩展现有的工具实现技术的方法，我们建议使用的现成的形式化方法工具作为属性语法验证的基础。O现成的工具可以以比扩展现有的求值器生成器低得多的成本提供显著的表达能力。作为一个具体的例子，我们描述了如何使用Alloy模型查找和检查工具来验证LIDO属性语法规范语言中的远程属性构造的属性。这种方法的一个天真的应用程序有显着的性能开销，我们讨论的技术，限制的范围内的问题，解决，使该方法易于处理。保留字：分类器生成，属性文法，形式化方法，软件验证。1介绍属性语法是一种用于指定编程语言和结构化文本的语义的完善的形式符号[1，13，14，16]。有许多方法可以从属性文法中生成有效的赋值器[2，10]。属性赋值器生成器通常关注从用户提供的属性语法中生成有效赋值器的核心问题。 在开发过程中可能有用但不需要生成评估器的外围功能通常被忽略。这类功能的示例包括浏览器，用于显示来自不同的1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.01134S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33用于发现或检查语法标记的形式属性的透视图或分析在其他当前的工作中，我们正在通过开发属性语法的集成开发环境来解决前一种功能，包括应用程序切片方法来方便查看[18]。本文主要研究第二类功能性：属性文法性质的形式化分析[3]。当然，赋值器生成器必须分析输入语法的各种形式属性以验证可以产生赋值器或产生正确的赋值器（例如，属性依赖性、循环性）。我们有兴趣提供分析，增加发电机提供的反馈。我们的技术可以应用于许多不同的分析。为了使我们的演示更具体，我们使用来自LIGA属性语法系统的LIDO规范语言中的远程属性构造的问题诊断作为运行示例[9]。其目的是在INCLUDING属性构造向上到达抽象语法树（AST）以从祖先节点获得属性值时提供适当祖先节点将不一定存在于树中。在这种情况下，我们希望向用户展示问题的示例，而不仅仅是错误存在的通知（LIGA的当前行为）。第2节提供了关于LIDO和包含问题的更多细节。而不是修改现有的属性语法系统，以增加额外的反馈，我们选择了一种方法的基础上，一个现成的正式方法工具。形式化方法为描述软件属性及其断言提供了一个表达平台. 属性和断言独立于特定的编程符号，因此可以编写前端以使分析工具能够与不同的语言一起使用。对于许多问题，可以使用形式化方法工具来实现有效的实现，比修改现有的生成器要少得多。这种策略还保持了整个系统的模块化，因为生成器可以专注于其任务，辅助工具可以为外围问题提供支持。我们的方法基于Alloy模型查找和检查工具[6]支持的形式关系模型。第3节总结了Alloy的相关功能，并讨论了它对我们正在解决的问题的适用性。该工具的一个重要方面是它能够提供反例来说明断言的违反。第4节提供了我们的方法的细节，包括以下主要步骤：(i) 要分析的属性语法被自动转换为一个模型规范，其中包括两个属性的语法在gen-S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3335分析中的特定语法的一般性和性质（4.1和4.2节）。 在我们的例子中，一般的属性包括这样的事实，即所有的语法都有一个单一的根非终结符，并且非终结符通过彼此相反的父关系和子语法特有的属性包括根非终结符的身份和非终结符之间的父关系，这是由语法的产生所暗示的。(ii) 我们希望检查的属性被表示为关于符合模型规范的模型的断言（4.3节）。所需的as- sertions自动从属性语法派生。在我们的示例中，对于每个远程属性构造，我们断言构造中命名的祖先节点必须在所有可能的AST中可达。(iii) 然后，模型规范和断言被传递给Alloy进行自动分析。Alloy继续生成符合规范的模型，并检查这些模型的断言是否为真。不满足断言的模型构成了一个反例。在我们的例子中，一个反例将由一个描述特定AST的模型我们将反例模型从Alloy表示法后处理回用户级表示法中的路径，以便在错误消息中向用户显示。可扩展性是软件形式化模型的一个重要问题基于形式化方法的 通常情况下，控制可伸缩性的关键是确保模型规范不过于具体。对于我们的例子，这意味着我们必须小心，不要试图建模完整的AST。相反，我们通过AST对路径进行建模，这允许模型忽略未出现在建模路径上的非终端。第5节评估了我们对属性语法的分析性能，该属性语法指定了Pascal子集的语义分析，并提出了进一步的修改，显着提高了性能。2LIDO和包含问题LIDO是LIGA属性语法系统的规范语言[9];反过来，LIGA是Eli语言36S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33\1 int n= int n;2 规则：dc：：= expr3dc.valuereturn value;4 结束语：5 规则：expr：：= expr6expr[1].value= ADD（expr[2].value，term.value）;7END;8 规则：expr：：= term表达式9expr.value= term.10 结束语：11 规则：term：：=数字12return value= digit;13 结束语：14 SYMBOL dc ZHANTE15printf（“%d n”，THIS.value）;16 结束语：图1. 台式加法处 理 器 生 成 系 统 [4] 。 LIDO1 源 自 ALADIN 语 言 ， 后 者 是 GAG 系 统（LIGA的前身）中的规范语言[8]。LIDO和ALADIN有许多共同的特性，主要的区别是LIDO只提供了一个通用的前缀风格来表达计算，而ALADIN是一个功能齐全的函数式编程语言。最值得注意的是，这两种语言都有包含结构，这是本文中解决的主要示例问题的核心。2.1桌面计算器为了解释LIDO表示法，图1显示了一个非常简单的属性语法，用于一个只使用加法运算符的台式计算器。语法计算输入表达式的值并打印它。LIDO可以使用ATTR关键字独立于符号引入属性，因此图1的第1行指定value属性为整数类型。定义如何确定属性值的计算与非终结符或规则相关联。在图1中，dc、expr和term符号的value属性的计算在四个规则中给出，其中产生式定义了它们的结构（第2-13行）。第12行中的终端数字的使用是指由词法分析器计算的终端的固有值。打印dc符号的值的计算与符号相关联，而不是与定义dc的规则相关联，因为它不需要引用dc符号的后代的属性（第14-16行计算使用前缀符号来调用语法符号之外定义的函数在这种情况下，库宏ADD是1有关LIDO及其在Eli系统中的使用的完整详细信息，请参阅Eli文档，该文档位于Eli分销商网站http：//eli-project.sourceforge.net上。S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3337抬笔抬笔抽血3平1*NEPNEP***下笔下笔*****平1取出5*******换行符换行符NEP图纸7抬笔换行符平2NEPNEP下 笔 画 3 新闻NEP图2. 简单绘图仪语言示例程序和输出用于执行整数加法，Cprintf函数用于打印 表达式的值2.2简单绘图仪语言在桌面计算器示例中，产品左侧符号的所有属性值都派生自右侧属性的值;也就是说，派生自树中的这是一种非常简单的归因模式。在更复杂的示例中，能够引用来自进一步移除的节点的属性值通常是有用的：在树中的当前符号上方或在以当前符号为根的子树中。图2左边的两列显示了一个用简单语言编写的程序，它需要这种处理。该语言允许控制一个键盘。笔可以被设置为向上状态或向下状态。在任一状态下，都可以使用DRAW命令将笔向右移动。 DRAW命令接受一个整数参数，该参数确定笔将向右移动多少个空格。当笔向下时，它将为它向右移动的每个空格绘制一个字符。当笔向上时，笔也会向右移动，但不会绘制任何东西。还有一个NEWLINE命令，将钢笔放置在下一行的第一个空格上。图中最右边的一列显示了程序.完整的简单绘图仪语言属性语法如图3所示.该语法使用Eli每个绘制命令都有一个pattern属性，用于保存该命令要产生的输出（第24和28行）。 绘制命令的模式被添加到第32行的pentrace就我们的目的而言，这个语法中最相关的部分是第25行中包含远程属性结构的使用。语言语义学38S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33\1ATTR模式： PTGNode;2CHAINpentrace：PTGNode; 34RULE：program：：=笔块5CHAINSTART HEAD.pentrace = PTGNRST;6int findDuplicate（int findDuplicate）;7结束语：8RULE：笔块LISTOF笔块END;910RULE：penblock：：=11pen block.pattern = pen modifier.pattern;12结束语：13RULE：笔修饰符：：=14penmodifier.pattern =PTGAsIs（“*”）;15结束语：16RULE：笔修饰符：：=17penmodifier.pattern= PTGAsIs（““）;18结束语：19RULE：commands LISTOF command END;20RULE：command：：= draw END;21RULE：command：：=penblockEND; 2223RULE：draw：：=24绘制模式=重复PTG（长度，25包括钢笔块图案）;26结束语：27RULE：draw：：=28int n =int n（n）;29结束语：3031SYMBOL draw符号32THIS.pentrace= PTGSeq（THIS.pentrace，THIS.pattern）;33结束语：图3. 简单绘图语言属性语法对于绘图命令，笔的状态将从直接包含draw命令的块。因此，当从绘图符号在第11行，pen block从它的pen modifier后代（第14和17行）获得实际模式2.3包括的问题简单绘图仪语言语法是正确的，但它说明了一个典型的情况下，很容易犯错误一个可能的初步尝试是具体说明包括：RULE：draw：：=INCLUSIVEpen modifier.pattern）;结束语：换句话说，我们试图从draw上下文直接访问pen modifier不幸的是，这种用法在静态上是非法的，S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3339pen modifier永远不会是draw的祖先。Eli系统处理此版本时，会产生以下错误消息。“spl.lido”，line 25，30：ERROR：在某些上下文中没有找到了包含符号的从这个错误信息中，很难诊断出问题。一般来说，它需要仔细分析抽象语法，以确定draw和pen modifier之间的关系。系统可以提供一个反例来说明问题，而不是仅仅通知用户错误。在这种情况下，一个反例将是某棵树中的一条路径，从包含（draw）的上下文到语法的根，它不包括所需的符号（pen modifier）。我们在本文其余部分描述的方法除了上面的消息外，还生成以下消息。“spl.lido”，第25行，第30行：例如，可以通过路径到达root绘图->命令->命令->笔块->笔块->程序“spl.lido”，第25、30行：笔修饰符符号将不会可通过在一些树中包含这些消息清楚地标识出有问题的符号以及违反INCLUSIVE静态要求的方式。有了这些信息，问题的原因几乎总是显而易见的。包含问题实际上比这里提出的更复杂。 LIDO还允许计算与符号相关联，的规则。此外，有可能有不出现在产品中的类符号，而不是出现在产品中的树符号，因此在AST中。类符号可以继承到树符号上，从而允许重用它们的属性。这种能力是LIGA支持可重用属性模块的核心由于类符号可 以 具 有 属 性 ， 因 此 可 以 具 有 INCLUSING 构 造 ， 因 此 任 何 诊 断INCLUSING问题的系统都必须考虑符号继承。2.4影响很容易设想其他有用的分析形式。例如，一旦用户收到上面的扩展消息，他们可能会想找到笔修改器和绘图的共同祖先。一旦确定了祖先，在这种情况下是笔块，图案就可以被传输到那里，然后可以使用包括从绘制中访问它。因此，对寻找共同祖先的支持是另一个潜在有用的分析。40S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33LIDO 支 持 其 他 远 程 属 性 结 构 。 CONSTRUMENT （ S ） 类 似 于INCLUDING，不同之处在于它在符号与树中当前符号下面的一个或多个其他远程符号之间创建依赖关系。 CHAIN构造创建一个线程化的依赖值链在所有的符号中，从左到右按深度第一的顺序通过树。这些构造具有类似的静态检查，可以以与本文中所示的包含问题类似的方式进行分析当考虑更大的语法时，本节所描述的自动分析的真正好处是显而易见的。如果属性语法包含几十个非终结符，由50-100条规则定义当语法由独立的模块组成时，这个问题会变得更糟，可能会引用库模块，或者当语法是由其他人在这些情况下，用户可能不得不搜索多个语法文件，其中一些或全部不是由他们编写的。相反，自动方法与系统的正常报告机制很好地集成在一起，不需要用户做额外的工作3形式化方法形式化方法已经被用来帮助软件开发几十年了，其目标是确保它满足其规定的要求。形式化方法分析工具，用于在或多或少的程度上自动化系统正确性的检查，可以分为两大类：证明助手和模型检查器。证明助手（也称为定理证明器）引导用户通过一系列与其软件规范相关的逻辑推理。包含复杂数据类型的系统可以使用证明助手的基于语义的语言来非常优雅地描述。特别是，像树木这样的有限结构对这些技术没有特别的阻碍不同的证明助手的自动化程度各不相同，但最终要么证明了一个断言，要么达到了一个无法进一步推导的点。如果证明是成功的，那么关于这个问题的大量信息就建立起来了，人们可能对结果有很大的信心。然而，如果证明不能完成，那么该技术提供的关于问题的附加信息很少，可以帮助开发人员进行软件开发。问题的原因可能在于正在开发的软件，但也可能在于证明策略本身。一般来说，成功使用一个证明S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3341助理需要开发人员的大量干预。像证明助手一样，模型检查器通常可以验证系统的正确性，但是与证明助手相比，模型检查器不提供关于正确软件描述的更多附加信息。然而，它们通常可以在没有开发人员干预的情况下使用，并且可以识别反例来说明断言的虚假性反例可以在软件开发过程中提供重要的帮助，因为它们指出了软件所需特性无法保持的特定情况。对于我们的目的，反例是至关重要的，因为它们构成了向属性语法开发人员提供更好反馈的基础最广为人知的一类模型检查工具对有限状态模型进行操作。符号模型验证器SMV是该类中的一个众所周知的工具[15]。SMV采用有限状态机的描述和表示为计算树逻辑（CTL）中的语句的规范，CTL是一种时态逻辑。 验证目标通过搜索实现由机器描述定义的状态空间。每当搜索发现不满足CTL规范的状态时，就会产生一个反例。反例是由一系列状态组成的，这些状态一直到那一点。从反例中的状态，开发人员可以确定机器违反其规范的情况静态模型是一种强大的规范方法，像SMV这样的工具能够搜索非常大的状态空间。这种方法最适合于验证复杂的并发系统，如通信协议或硬件架构，其中状态的概念是普遍的。我们已经将这种方法应用于属性语法建模，但发现我们想要建模的属性语法概念与有限状态机概念之间的语义差距太大。在属性语法分析中，根据状态和状态变量进行思考是不自然的，SMV不支持从底层基于状态的模型中抽象出来的机制。我们能够用SMV来制造反例，而具体化是不直观和笨拙的。相反，我们的工作基于Alloy工具2，它提供了上述两种形式方法的一些优点[6]。Alloy规范语言使用一阶关系逻辑，是声明的，并且基于形式规范语言Z [17]。与Z不同，Alloy规范可以自动分析，其方式与模型检查器分析有限状态机规范的方式大致相同就像基于有限状态模型的模型检查器一样，Alloy提供了反例2Alloyisavaailablea t http：//alloy. mit.edu.42S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33{来说明不满意的断言。Alloy因此，该方法是根本上不完整的意义上说，一个过小的范围可能会阻止一个反例被发现，我们不相信这是一个严重的问题，因为我们的方法，我们不依赖于模型检查器的能力来检测错误，而是说明错误，已经知道存在。我们将在第5节讨论范围选择问题。与有限状态模型检查器不同，Alloy因此，Alloy此外，由于语法不是动态系统，而是静态结构，因此Alloy3.1合金实例本节通过一个简单的族模型规范来这个例子是基于Alloy发行版提供的示例代码。我们将非正式地介绍合金符号，因为在大多数情况下，它们与逻辑和数学关系的众所周知的概念密切相关。Alloy手册包含了规范语言语法和语义的完整描述[6]。家庭模型的具体化首先是指定一类代表人的原子。签字人配偶：选项人，父母：设置人}上述陈述通过宣告人们参与的关系的“签名”来宣告一类人。一个人p与他们的配偶（也是一个人）有关，并且与一组人有关，这些人是p.配偶关系是可选的（即，可能是空的），因为不是所有的人都有配偶。我们将人的类划分为男性和女性的子类，part sig Man，Womanextends Person{}事实是关于集合的成员资格的陈述，以及集合中原子之间的关系，这些关系对原子的所有排列都是真实的例如是S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3343{{没有人可以成为自己的祖先的生物学事实可以写成：事实生物学no p：Person |p中的p。父母}用更数学的话来说，这个事实表明，不存在这样的人的类的成员p，使得p在通过对从p开始的父母关系取传递闭包而形成的集合中。关于配偶关系的社会规范的事实可能包括：• 配偶关系是对称的（波浪号代表给定关系的转置）。所有p：人|p.配偶= p.~配偶• 没有人是他或她自己的配偶。no p：Person |p.配偶= p• 男人男人.配偶在女人.配偶在男人我们可能想看看我们的模式是否禁止通婚。我们定义这意味着没有人的配偶是他们的兄弟姐妹或他们的父母或其他直系祖先。上面没有一个事实以这种方式明确地限制模型，但是我们可以通过将需求指定为断言并搜索断言的反例来检查它们是否隐含地定义了这种限制。以下是一个可能的断言：主张不通婚no p：Person|一些p.配偶&&（（有的p.配偶.父母&p.父母）||（p.配偶在p.^父母））}换句话说，这个断言说，如果配偶与p有共同的父母，或者配偶是p的祖先，那么就没有人p有配偶。当提供模型规范和断言时，Alloy生成满足规范的模型，并检查断言在每个模型中是否为真。理解事实和断言之间的区别是很重要的。事实指定了模型必须遵守的约束，以符合规范。Alloy不会考虑不符合事实的模型。断言指定了我们期望持有的属性，但对于某些模型可能实际上并不持有。由于典型的规范描述了潜在的无限结构，因此有必要限制用于生成模型的类的范围。在我们44S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33例如，我们必须限制Person类的大小;换句话说，我们必须指定要检查的模型中的最大人数对于这种情况，断言在某些Person类的作用域仅为3的模型上失败。Alloy生成的反例是显而易见的：人0是人1和人2的父母，人1和人2是彼此的配偶。了解到现有的约束是不够的，开发人员可以向规范添加额外的约束，以确保不允许这种情况显然，模型的范围问题对于Alloy的实际验证很重要。必须限制作用域，以便方法易于处理。 Alloy是通过将模型规范转换为一个布尔表达式，传递给一个现成的SAT求解器[5]。SAT求解技术目前非常强大，但仍然限制了可以实际分析的表达式的大小。通过限制Alloy模型中底层集合的范围，我们可以限制必须求解的表达式的大小。当然，这种限制意味着核查并不完整。即使Alloy没有找到反例，也可能有更大的模型违反断言。在实践中，经验表明，易于处理的模型大小表面上可以用现实的模型规范来发现问题[7，12]。4模拟包容问题现在我们转向使用Alloy规范语言对第2首先，我们考虑如何捕获所有属性文法都具有的属性，这些属性是解决包含问题所需要的。然后，我们考虑使用第2节中的Simple Plotter Language语法作为示例，使用特定属性语法的细节来扩展规范。一旦规范完成，我们将展示如何表达关于包含构造的静态需求的断言。然后，我们描述了如何扩展该模型来处理LIDO本节中描述的技术与特定的属性语法表示法无关。它们已经体现在一个Eli-specific工具中，该工具将LIDO属性语法转换为Alloy规范。因此，分析过程是完全自动的。我们将在下一节中评估Eli环境中的方法。4.1属性文法的一般性质为了我们的目的，属性语法的相关属性涉及符合底层上下文无关语法的AST中的本S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3345}个字符。签名GGRNG[s]根：%s，父级：s ->s，子级：s -> s//child是parent child=~parent的转置//没有n：s |n在n中。孩子//root中没有断开连接的组件。*孩子}图4.AST中非终端符号之间关系的合金规范最后，我们对AST中的非终结符之间的关系进行了建模。存在区别的根非终结符和非终结符之间的父关系如果X出现在一个产品的左侧，而Y出现在同一个产品的右侧，则非终结符X是非终结符Y的父代。除了根之外的所有非终结符都至少有一个父终结符。终端符号被忽略，因为它们在LIDO中不能有关联的属性，因此图4示出了父子关系的合金规范GGG这种特殊性在s中是通用的，s是代表非终端符号的原子类规范的第一部分声明了相关关系：表示根的一元关系，然后是二元父关系。有些属性用子关系比用父关系更容易声明，所以我们也声明了。在签名之后是事实（或约束），它必须始终对每个GGBLOG实例保持。首先，子关系只是父关系的转置，因此只需要显式地定义其中一个。其次，我们3最后，我们通过要求所有符号都可以从根访问来GGTIF定义了所有非终结符之间的关系。对于包含问题，我们需要能够讨论这个图中的特定路径。下面的规范建立在GGALO签名的基础上，没有添加任何关系，但添加了一个事实，即将路径模型限制为每个符号最多有一个子节点的模型。对于任何一个GGPath实例，都可能有许多GPath实例代表从符号到根的所有不同路径。[3]请注意，这个决定是由包含问题的性质所证明的我们{46S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33{int [s] extends int [s]{}个字符。所有n：s|独生子女}最后，我们声明一类符号。这个类充当占位符，并将在下一节中通过语法中的实际符号进行扩展签名符号{}4.2特殊属性文法的性质特定属性文法的模型符合上一节中的规范，但也必须提供细节来填补这些规范中的空白：符号的身份（包括哪一个是根）以及父关系或子关系的性质文法的非终结符通过扩展通用Symbol类来声明。4我们要求一个特定符号的类与其他符号的类不相交（由disj关键字表示）;否则，Alloy将允许将不同符号等同起来的模型。disj sig program，pen blocks，pen block，pen modifier，commands，command，drawextendsSymbol{}由于我们不需要考虑递归构造，我们可以限制每个符号类最多包含一个原子。这一限制大大减少了搜索空间的大小。事实上，在MostOne唯一的程序唯一的笔块...}根符号的同一性和父关系或子关系的性质是由一个关于GGG规范的所有实例g的事实来指定的，该实例g是用符号类s是Symbol来指定的。我们选择显式定义子关系，因为它比父关系更直观;父关系由前面给出的转置约束隐式定义。科.事实{4在下文中，我们假设LIGA标识符可以安全地直接用于合金规范。在实践中，需要对语法进行一些修改，以确保这些使用是合法的。S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3347所有g：GGALO[Symbol]| g.rootin程序&&例如，儿童在（程序->笔块+笔块->笔块+笔块->（笔修饰符+命令）+命令->命令+command -> draw +command -> penblock）}事实主体的第一部分说，它涉及所有的GGALG [符号]图G.然后我们指定程序是g的根。那么孩子的关系通过枚举上下文无关语法给出的组成对来定义;例如，该对（程序，笔块）处于子关系中，因为生产程序：：=笔块。4.3关于远程归因的断言最后，我们需要在属性中表达描述INCLUDING构造的静态需求的断言。5在错误的简单绘图仪语言示例中，只有一个包括：RULE：draw：：=INCLUSIVEpen modifier.pattern）;结束语：这个INCLUDING隐含的要求是，从一个drawcontext中，总是可以进入AST并找到一个pen modifier节点。我们可以这样表述这个要求在Alloy中成立的断言：assertdrawIncludespen修饰符allp：GPath[Symbol]|所有x：绘制|一些y：笔修改器|x中的y。（p.parent）}5INCLUSIVE的一般形式允许指定多个属性，在这种情况下，如果任何一个指定的符号在任何AST中作为祖先存在，则该构造是合法我们的方法很容易扩展到处理多个符号在pseuduudings，但我们省略了空间的原因的细节。{48S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33换句话说，对于图中的所有路径，对于绘制符号的每个实例，必须有一个笔修饰符，该笔修饰符位于从绘制开始的路径父关系的传递闭包中当我们看到前面两节中的模型规范和这个断言时，我们可以让Alloy搜索符合规范但违反断言的模型。我们使用下面的Alloy检查语句来约束模型的范围，使其包含不超过5个符号，因为从任何符号到该语法的根的路径中不能有超过5个符号。此外，我们只使用一个GGPACK实例，因为它可以在所有路径之间共享检查drawIncludespen修饰符，用于5但1个GGBLOG [Symbol]一个违反断言的模型包含以下子关系：p.child =（程序->笔块+笔块->笔块+笔块->命令+命令->命令+命令->绘制）这符合以下错误路径：绘图->命令->命令->笔块->笔块->程序4.4建模符号继承到目前为止，我们的模型规范只处理树符号。我们必须添加继承关系的建模，以便能够正确处理在类符号属性中出现的包含构造，或者将类符号引用为必须存在的祖先符号。图5显示了前一种情况的一个简单示例。树的符号是A、B、C和D（第2-7行）。唯一的类符号是Q（第9行），它被继承到D（第8行）。Q. value的计算使用了一个INCLUDING来从B祖先中获取值（第10行）。如果与Q相关联的D是从B导出的，那么包含是合法的，但是D也可以从C导出，然后从A导出，在这种情况下不存在B为了对符号继承进行建模，我们使用以下两个相互转置的关系来扩展基本图模型：已签署的GGG [s]...继承：s-> s，{S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3349{1 int n= int n;2 规则：A：：= B3B.value = 1;4 结束语：5 规则：A：：= C结束;6 规则：B：：= D结束;7 规则：C：：= D结束;8 树形符号D继承Q结束;9 类符号Q TE10INH.值= ADD（包括B.值，1）;11 结束语：图5. 使用符号继承的简单属性语法。inheritedby：s -> s...继承=~inheritedbys in root.*孩子+（root.*儿童）。*继承}我们还扩展了可达性事实，以包括通过继承关系到达符号的可能性这确保类符号连接到模型的其余部分。GPath和Symbol的定义与以前一样。为了区分树和类符号，我们为符号类添加了额外的区分级别，并确保没有其他符号。disj sigTreeSymbol，ClassSymbol extends Symbol{}事实{Symbol = TreeSymbol + ClassSymbol}语法中的实际符号然后适当地扩展TreeSymbol或ClassSym- boldisj sigA，B，C，Dextends TreeSymbol{}disj sigQextends ClassSymbol{}文法的根和子关系如前所述被具体化，但通过D和Q之间的继承关系的具体化而被扩充。事实所有g：GGALO[Symbol]|根A&&例如，（A->（B+C）+中的儿童B->D+C->D）&&}个字符。50S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33{{例如，在（D->Q）}由于Alloy可以选择从特定路径的模型中省略任何符号，因此会出现一个轻微的复杂情况但是，如果其中一个符号继承了一个或多个类符号，那么我们必须确保这些类符号也在模型中。否则，我们就不能正确地对包含引用继承到祖先符号上的类符号的情况进行建模。对于这个例子，我们需要以下额外的约束：1）如果模型中有D，那么也必须有Q，2）如果模型中有D，那么每条路径都应该有D和Q之间的继承关系。事实D => Qsome D => all p：GPath[Symbol]|（ D -> Q）在p.继承}为了表达图5第10行中包含的要求，我们使用以下断言。断言QIncludesB所有p：GPath[Symbol]|所有x：Q|sommey：B|y在（x.*（p.inheritedby）.^（p.parent）.*（p.继承））}它与前面的形式相同，只是它遍历继承关系以及父关系。最后一行的要求确保我们遵循从Q到继承Q的任何树符号的继承关系，然后通过这些树符号的父关系向上AST，然后包括继承到我们找到的祖先树符号的任何类符号。使用此断言，我们可以使用以下命令检查QIncludesB是否有3个但有1个GGBLOG [Symbol]而Alloy会发现以下反例：Q-> D-> C-> A5评价我们早期开发模型的尝试要求我们一次对整个语法建模这被证明是一个糟糕的策略，因为它会导致模型S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）3351其规模大到难以生成和检查。在非平凡文法上，我们总是放弃等待Alloy产生反例。我们在本文中提出的版本通过仅对路径进行建模来弥补这一缺陷，这些路径通常包含比整个语法少得多的符号。换句话说，symbol类所需的作用域只需要足够大，以处理最长的可能非递归路径。对于real- istic文法，我们可以预期这大约是10到20个符号。表示未出现在路径上的符号的关系可以为空，它们我们的主要评估已经在对Pascal的子集执行语义分析的语法上执行[19]。文法有52个产生式，使用68个树符号和25个类符号;类符号主要来自库模块。语法中有36个包含结构。我们在Apple Powerbook G4上运行了我们的实验，该Powerbook G4具有1 GHz处理器和1GB RAM，运行Mac OS X 10.2.6。我们开发了一个Eli包，当LIGA报告包含问题时，用户可以调用它。我们实现了一个转换器，它采用LIDO属性语法并将其转换为第4节中描述的Alloy规范。6（对于Pascal子集语法，Alloy规范在几秒钟内生成。Eli包翻译用户如果合金未能产生一个反例，那么用户将只看到原来的LIDO消息。我们定时正确的Pascal子集语法的分析，以确定最坏的情况下的时间。7我们目前的测量结果表明，有可能在大约20分钟的用户时间内（范围为10）或34分钟的用户时间内（范围为15）分析所有36个数据库。（两个不同的作用域产生相同的结果。）这些时间从4.2节描述的决定中受益匪浅，限制每个符号类最多包含一个原子。如果没有这个限制，使用范围10进行全面分析需要20多个小时。我们希望我们的方法是最有用的，一旦一个特定的问题，包括已被诊断的一些其他方法（例如，来自LIGA的消息）。因此，一个更现实的用例是一次只分析一个INCLUSION。我们检查了测试用例中的各个子模块，6我们当前的翻译器没有实现LIGA语义的一个方面：如果符号X继承自符号Y，并且Y有属性的定义，那么X可以覆盖该定义。如果Y7我们没有观察到任何内存消耗问题，因此我们52S. Goldrei，A.Sloane/Electronic Notes in Theoretical Computer Science 110（2004）33确定了占用分析时间比例最大的一个。它需要大约24秒的范围为10或一分钟的范围为15。这些时间并不完全产生交互性能，但对于需要诊断的罕见情况来说是相当困难的在正在进行的工作中，我们希望看到性能改进，原因是：(i) 仅建模错误的包含构造。我们当前的模型规范包含了所有INCLUDING的语法和断言。一个更好的策略是将模型定位于只解决那些触发LIGA错 误 的 错 误 。 我 们 希 望 看 到 ， 对 于 合 理 大 小 的 语 法 ， 对 于 单 个INCLUDING问题的诊断时间大约为10秒(ii) 更准确地设置模型的范围。目前，我们对所有语法都使用固定的作用域一个更好的方法是计算一个特定文法所需的最大范围，这样我们就可以保证没有反例被遗漏，但限制了必须做的冗