可在www.sciencedirect.com在线获取理论计算机科学电子笔记304（2014）97-110www.elsevier.com/locate/entcsK语言中语义分析的抽象语义IrinaM.P.AriucaAs.V.OAE3计算机科学学院大学AlexandruIoan CuzaIaCuzasi，R omania摘要本文提出了一种在K框架中集成分析和验证方法的方法我们采用抽象解释的视角，即将被分析/验证的具体系统映射到一个合适的抽象系统，并在抽象系统上应用收集语义来获得分析/验证方法本身。因此，我们提出了K的角度收集语义K操作语义的抽象系统。为了更好的一般性，我们认为抽象系统是（有限）下推系统的K个具体化我们给出了收集语义作为一个通用的一组K规则参数化的K规格的有限下推系统。此外，我们描述了一个案例研究，实例收集语义与别名分析。为此，抽象系统被定义为一种命令式语言，它维护了足够的指针和数据流信息，以便别名分析是可判定的。这种命令式语言的K规范适合有限下推系统规范的框架关键词：抽象，收集语义，下推系统，别名分析1介绍K框架[14]的火花是观察到计算是通过重写自然表达的。K的灵感来源于重写逻辑语义学项目[9，19，10]，该项目的目标是统一代数指称语义和操作语义。这种统一是通过将两种语义视为同一对象上的不同视图来实现的。也就是说，指称语义将语言的重写逻辑规范视为指定模型，而操作语义则关注同一规范的执行K是建立在一种基于延续的技术和一系列符号约定之上的，以允许更紧凑和模块化的编程语言定义。K定义可以被机械地翻译成重写逻辑，特别1合同ANCS POS CCE，O2.1.2，ID编号602/12516，ctr.nr 161/15.06.2010，DAK。2罗马尼亚欧洲社会基金，由2007-2013年人力资源开发部门业务方案管理局负责[赠款POSDRU/88/1.5/S/47646]3电子邮件：mariuca. info.uaic.rohttp://dx.doi.org/10.1016/j.entcs.2014.05.0051571-0661/© 2014由Elsevier B. V.98I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97进入Maude，获得基于术语重写的程序分析工具或解释器。这种能力使K成为一个可执行的框架，K-Maude是它的原型实现[15，18]。K定义是一个转换系统的可执行规范，其计算是通过执行K定义获得的。此外，还可以重用K定义以实现更丰富的执行，例如计算集在生成普通计算时，K可以被看作是一个解释器，而在生成计算集时，K也可以被用作特定转换系统的分析器/验证器这是当前的文件在一个简单的想法，我们框架下提出的抽象解释的方法在抽象解释中，一种特殊的分析/验证方法是通过定义所检查的转换系统上的集合语义来实现的[4，5]。也就是说，转换系统首先被转换成一个更简单的然后，收集语义依赖于抽象转换系统的操作语义，并通过向前或向后定点迭代收集其计算。因此，分析/验证方法是操作语义的语义反映。1.1捐款汇总在本文中，我们提出了一个基础设施，表示在K的反射的操作语义到收集语义，别名分析实例化的反射。这个基础设施的基石是选择下推系统作为合适的K定义。通过配置抽象机制和定义模块化，语义反射在K选择下推系统作为本研究的焦点是由于概念的普遍性，已经获得的理论结果以及与K定义的密切相似性。通过后一种相似性，我们的意思是K中使用的基于延续的技术为k单元提供了堆栈方面，而K规则通常依赖于下推堆栈机制。在第2节中，我们提出了下推系统的分析/验证方法的K更详细地说，在2.1节中，我们讨论了下推系统的K在2.2节中，我们使用下推系统的K规范作为推导分析/验证基础设施的支持。我们还在2.3节讨论了考虑下推系统及其K规范的机会。在第3节中，我们通过K规范介绍了一种具有过程和对象的抽象命令式编程语言SIL stecK的SIL stecK在K框架的上下文中很有意义，原因如下• 这是在[17，16]中引入的一种研究语言，具有几个双相似语义。在3.1节中，我们给出了这些语义之一的K规范。特别是，这种语义展示了算法细节，强调了K在算法制定领域的多功能性。I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）9799• SIL steck的这种特殊语义具有产生有限可达状态空间的有用特性。使用这种语义带来的好处是分析/验证方法的可判定性。在第3.2节中，我们将别名分析作为第2.2节中分析/验证的一般方法的实例。目前的工作开始的任务是给出一个忠实的K规范， 在[17，16]中提供的[17，16]的作者给出了作为下推系统规范的语义。因此，通过下推系统对SIL stecK工作的方法论观点自然出现（第2.1节）。此外，由于其基于连续的特征，K被证明是下推系统的合适的规范环境（2.3节）。SIL steck作为别名分析的抽象的观点是这项工作中的实际新颖性。我们在2.2节中将其作为下推系统的方法论，并在3.2节中作为方法论的实例。1.2相关工作当前工作的核心是[17，16]中给出的语义学研究以及与[17，16，2]作者讨论中提出的想法。我们借此机会感谢在[2]上的丰富合作，其中SIL steck扩展了字段，并使用Maude LTL模型验证程序[6]，通过对堆属性的常规语言进行有界模型检查。请注意，单纯的语法扩展涉及语义上的剧烈变化。因此，SIL steck在语义上不同于[2]中提出的抽象语言这里所讨论的程序分析方面是对[1]中提出的思想的一种改进。在K中的程序分析的早期工作在[8]中提出，其中分析作为程序断言语言的抽象语义给出。这项工作演变成匹配逻辑提出的演绎验证工具[11，12，13，20]。目前的方法的主要区别是，我们提出了一个抽象的语义，这是从实际的代码解耦，在风格的抽象解释。K框架的冠军语义是[7]中描述的C的规范。在那里，使用Maude [6]中提供的继承模型检查功能测试语义的有效性，并使其用于程序验证。在这种情况下，关于别名分析，我们把工作作为证据，[21]其中C被抽象为上下文无关的，对等式和别名分析不敏感的语言我们在SILsteck中提供了类似的方法，唯一的区别是别名分析是跨过程的，并且对数据流敏感。2基础K定义通过配置和应用于配置的规则来指定某类过渡系统然而，当为了分析/验证的目的而对这些过渡系统进行推理时，通常情况下，100I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97我们需要将这个类限制为有限个迁移系统。在第2.1节中，我们提出了一个K透视图，它覆盖了一类有限的潜在无限变迁系统，由有限下推系统给出。关于有限下推系统的推理的可判定性结果的存在是它们在K中集成的进一步激励。我们将在2.2节中利用这些结果。在2.3节中，我们强调K定义风格导致语言的K规范与下推系统之间的自然相似性2.1下推系统K-规范接下来，我们提出一个一般的技术，指定下推系统在K，通过抽象。首先，我们建立了有限下推系统的K规范的框架。 然后，我们描述如何将无限下推系统转换为有限下推系统的K规范。这种转换是作为抽象给出的。回想一下，下推系统是一个四元组P=（Δ， λ，<$→，c0），其中Δ是一组控制位置，λ是一个堆栈字母表，<$→是（Δ× λ）×（Δ×λλ）的子集，表示规则集。一个构形是一个对（δ，Γ），其中δ∈ Δ且Γ ∈π。所有配置的集合记为Conf（P），c0∈Conf（P）是初始配置。一个下推系统被称为有限的，当集合Δ，ε，<$→是有限的。一个下推系统等价地由它的相关跃迁系统T P=（Conf（P），→，c0）描述，其中有→ n（Δ × n ∞）×（Δ × n ∞）.关系→被定义为如果（δ，γ）<$→（δJ，Γ）则（δ，γΓJ）→（δJ，ΓΓJ），对于所有的ΓJ∈Δ，其中δ，δJ∈Δ，γ∈γ，且Γ∈γj。为了在K中定义一个下推系统P，我们首先假设我们有Δ和Δ的代数表示K构型将Conf（P）的结构描述为一个标记细胞的嵌套袋，即标记ΔcKkP。K的基于连续性的特征由特殊的单元格k引入，它包含一个特殊排序K的计算任务列表。在P的K定义中，我们通过K语法命令K：：= K指定K是K的子排序当r = γ1..在计算单元中引入γn∈ ε n，它变成了εγ1a。aγnk，其中a是计算任务的K分隔符有限下推系统的规则变成K计算规则如下：任何 （δ，γ）<$→（δJ，Γ）我们有K规则<$δδJ中国科学院Γ·······出现在上述规则中的K的一些符号元素包括椭圆和局部重写。细胞壁上出现的椭圆···代表该细胞的某些未指定内容。例如，k中的省略号使γ成为延续堆栈的顶部，而堆栈的其余部分则由···编码。 注意在 根据上述规则，δ代表细胞的全部内容。局部重写（用二维符号指定）触发对配置进行的局部更改。因此，k单元中的重写表示γ的I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97101通过堆栈中的等价的重写规则（也可以用K表示法）是δcγaΓjkδJ cra Γjk，即，转换系统TP中对应的转换子集。转换关系<$→被指定为K规则的有限集合。 对于定义K规则，广义有限模式集Δ2Δ，Δ2Δ。正在重写在环境中，这些模式自然是使用变量来描述的我们表示这些模式asδε ∈Δε，带素数或带下标，γε ∈Δε，带素数或带下标。 也r =γ0。其中n∈N，γ n具有性质γ0.n.γn=γ0.. γπn。无限下推系统的关系<$→的K规则被定义为：对于任何（δ，γ）<$→（δJ，Γ），有一个规则δδJ电子邮件：info@hzc.com···这样做，δmatchesδandγ matchesγ，δJ matchesδJandΓ matchesΓ我们将Δθ和Δ θ中的每一种模式都归为一个唯一的常数，并表示为kP由以下配置给出的有限下推系统的K规格：最后，我们将讨论两个问题：注意，kP是f P的抽象。 THE这种抽象的粗略选择是由模式的有限集合Δk={，Δ}和={，}。2.2下推系统K-规范我们描述了一个通用的方法分析/验证问题P| = P，其中P是P的感兴趣的性质。我们使用在抽象解释中建立的设置，其中T |= T被定义为集合语义[4]，其中T是一个转换系统。也就是说， 同样地，我们的目标是详尽地执行kP，并沿着这个执行收集感兴趣的信息。注意我们可以推断出P|只有当kP是P的一个合理的抽象时，才能从k P的收集执行中得到k P。然而，这方面超出了本文件的范围基于[3]中的结果，如果在有限下推系统中存在无限路径，则这是套索形状的，即，这条路径有一个前缀，以循环结束。也就是说，无限路径呈现如下的重复堆叠模式102I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97C0→C （δ，γY）→w（δ，γXY）→w（δ，γXXY）.任何一条不归路，套索形状）的特点是有限的前缀（即，r是一个新项，使得（δ，γXrY）=（δ，γXY）。例2.1我们考虑P0=（{x，y}，{a，b，c}，<$→0，（x，abc））一个下推系统，I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97103P其中关系<$→0由以下集合定义：{（x，a）<$→0（y，a），（y，a）<$→0（x，bca），（x，b）<$→0（x，bca），（x，c）<$→0（y，bca）}P0中唯一的计算是：（x，abc）→a（y，abc）→a（x，bcaabc）→b（x，caabc）→c（y，aabc）→a（x，bcaaabc）→b（x，caaabc）→c（y，aaabc）。 .因此，我们将δ的套索标识为y，γ标识为a，X标识为a，Y标识为bc，w标识为abc。这个计算可以用它的有限个prefix来表征（x，abc）→a（y，abc）→a（x，bcaabc）→b（x，caabc）→c（y，aarbc）我们的目标是开发一种技术，用于重用下推系统的K-定义，以获得收集语义，使用前向定点迭代。kP的收集语义的配置，记为kP，定义为：⟨⟨⟨Δ˘⟩ctrl⟨K⟩k⟩trace∗⟩traces⟨⟨⟨Δ˘⟩ctrl⟨K⟩k⟩trace∗⟩traces′⟨Bag⟩collect其中Bag是预定义的K排序。单元格trace和traceJ旨在指导重写，以获得广度优先的穷举执行。因此，跟踪包含当前的执行级别，而在跟踪J中，我们构造下一个级别。广度优先策略相当于在重写规则的应用中强加公平。像往常一样，我们需要一些公平性条件来确保定点迭代的单调性。为了获得收集语义的规则，我们首先识别并分组kP中的规则，如下所示：对于eachγε∈εε，δε∈Δε，考虑所有规则小行星δ⟩ctrl⟨ γ˘Γ˘i···k，0≤i≤n，其中n∈N是n δ εεεctr lεγε···εk的不确定性因子。We 表 示 由 ypost （ <$δ<$i <$ctr l<$γ<$a<$j<$k ） 表示 的 集合 {<$δ<$i <$ctr l<$γ<$ia<$J<$k|0≤i≤n}。我们在图1中的K规则中使用post运算符。1、关系式在收集单元格的内容物上，Bag × Bag是有根据的。请注意，可以使用sear c h命令“search：搜索δP=>1搜索D：ΔK：KP“来获得帖子（δγk）。图1中的收集规则模拟了一个共享内存模型，其中的单元收集是共享内存。定制收集单元格的内容，以保持分析/验证方法的预期结果。 第一条规则通过消耗来自轨迹的当前计算轨迹并在轨迹J单元中产生新的计算轨迹来编码k的穷举执行步骤，前提是该步骤增加了收集单元的内容。第二个收集规则涵盖了当前选择的跟踪没有基于给定的更新操作增加收集单元格我们还没有具体说明收集单元格，因为其结构和更新操作取决于目标104I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97规则···δctrlγajk迹·电子邮件···追踪····post（δctrlγa<$jk）电子邮件······update（Bag，<$δ<$$>c <$$>γ<$a<$$>J<$k）当Bag更新（Bag，<$δ<$$>c <$$>γ<$a<$$>J<$k）时，规则···δctrlγajk迹····追踪袋收集当Bag/update（Bag，<$δ<$$>c <$$>γ<$a<$$>J<$k）Fig. 1.在KP上的集合语义的K规范的规则。分析/验证方法。在广度优先穷举执行中，切换到下一级计算是由以下规则完成的当NextLevel·时，规则将跟踪NextLevelbag2set（NextLevel）·其中操作符bag2set从NextLevel中删除重复的元素。在k P中设计的P的“穷举”执行的终止如前所述，下推系统中的无限计算呈现出由套索形状给出的重复模式。细胞收集基本上是由各种表示或抽象的计算prefixes显示的穷举广度-第一次执行的kP。因此，收集单元中收集的计算轨迹可以以套索形状为轴，并且一旦特定计算识别出套索的循环，就停止更新通过对收集单元的内容的这种设计，关系可以是简单的包含，因为更新操作确保了包含的良好基础。因此，由于kP中的计算要么是有限的，要么被简化为有限个前缀，因此收集计算终止。2.3下推系统与程序设计语言语义的关系我们现在讨论在编程语言语义学的背景下研究下推系统的相关性。K框架是专门为编程语言语义的规范而设计的。这种规范的最大优点是我们有一个直接基于I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97105语义然而，请注意，只有当语义为某个程序实例化时，才能看到解释器在工作。在这一点上，当一个程序在行为上与下推系统等价时，下推系统显示出理论上的相关性。因此，设计一种K中下推系统的分析/验证方法，就等于给出了一种K中定义的程序设计语言的分析/验证方法。考虑一种语言和该编程语言中的程序P的语义的K规范S。根据[20]中提供的用于设计S的方法，k单元表现为堆栈，而控制位置由包含存储器和程序的单元维护。在这种观点中，语义S等同于由S的语法部分产生的下推系统的规范，作为堆栈语言，除了k之外，所有的单元都是控制位置。然而，请注意，存在限制，例如，必须始终在顶部进行k尽管如此，从分析/验证方法的角度来看，为具有规范S的程序P无限下推系统通常通过一个合理的有限投影进行抽象解释来处理，该投影具有足够的表达能力，可以为感兴趣的分析/验证方法提供所从状态抽象的抽象解释的角度出发，利用元算子将下推系统的控制位置强制转换为有限框架此外，[5]表明抽象元运算符也会引起句法元素的栈语言）。这种转换是很自然的，考虑到一些句法元素的目标部分，抽象出的控制位置。例如，假设某些分支条件依赖于某些变量的当前值，但抽象消除了变量的实际值。然后，通常将分支条件抽象为不确定性选择，并将其语义替换为抽象语法元素的语义因此，抽象元运算符也必须将S中的规则从抽象语义转换为等价的（抽象的）规则3一个简单的命令式语言与对象创建在本节中，我们将介绍SIL stecK-一种简单的块结构编程语言的K规范，它支持对象创建，全局变量，静态范围和带有局部变量的递归过程。该语言在[17，16]中作为下推系统规范进行了介绍和研究。在这里，我们在图2中给出了SIL stecK语法的忠实K表示，在3.1节中给出了语义。这种语义在[17，16]中被称为因此，我们可以在这个抽象语义上应用收集语义。在3.2节中，我们使用别名分析来收集语义。请注意，我们选择别名分析，因为SIL stecK的控制状态侧重于维护所谓的别名类。SIL steck程序由一组有限的程序组成，这些程序作用于一些全局和全局的，106I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97Pgm：：=gvars：Idslvars：Ids{Procs}Ids：：=List{#Id，进程：：=进程ID：：B|ProcsProcs ProcId：：=#IdVExp：：=#IdBExp：：=#Id=#Id | #Id /=#IdB：：= VExp：=VExp|VExp：=new|B;B|[BExp]B|B+B|ProcIdIntBot：：=#Int|⊥图二. SILsteck语法局部变量集。SIL steck是静态作用域的。在过程调用时在过程返回时赋值语句x：=y将存储在y中的标识（如果有的话）赋值给x，而语句x：=new创建一个新对象，该对象将由变量x引用。顺序组合语句B1、B2和条件语句[b]B有标准的解释.非确定性选择被实现为两个计算规则，将B1+B2减少到B1或B2。3.1SIL steck抽象语义在本节中，我们将描述SIL stecK抽象语义的K规范，即，定义用于别名分析的有限下推系统的语义出于可判定性的原因，收集语义必须与有限状态模型一起工作。特别地，[16，17]中提出的抽象语义使用具有抽象内存地址的内存分配协议。因此，SIL stecK状态将来自集合的某个抽象内存地址与每个指针变量相{10}11.. 2 |VG|+的|Vl|得双曲余切值. |VG|和|Vl|分别表示全局变量和局部变量的数量，并且与unfined对象相关联。因此，SIL stecK程序的状态空间是有限的，因为程序有有限数量的指针变量，无论是全局的还是局部的。抽象修改了有关内存分配的语句，即对象创建、过程我们设计了一种定义抽象的机制，它保持语法元素在k单元中的位置，并将抽象计算分派到一个特殊的单元kAbs中，如图1所示。3 .第三章。因此，每个语句的抽象语义被指定为两个阶段：ping和ped。ping阶段由结构规则实现，该结构规则在kAbs单元中推动下一个抽象状态的处理ped阶段识别已经接收到kAbs单元中的下一个已处理的抽象状态的事实，因此它执行更新存储器和k单元的顶部的转换ping操作符有一个等式实现，以ped结尾标准形式因此，ping-ped机制将抽象a laabestheticin interpretationintoanequationalabraction. 这种转换反映了两个抽象的继承正交性。也就是说，I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97107⎜⎝⎟⎠⎜⎟ruleX：= new···kSstateNsize·kAbs北京赛车pk10开奖结果[结构]ruleX：= new····双态双肽S ·[过渡]ruleP···kSstateGgvarsLlvars·kAbspingSsigmaGgsLlscal[结构]规则集B恢复（S）[过渡]···SJ双态噬菌体SjkAbs P›→B···Pgm·规则⎛⟨restore(SJ)···⟩k⟨S⟩state⟨G⟩gvars⎞公司简介pingSsigmaSJsigma1Set（G）gi−gnSet（G）g1−gnSJsigmairet[结构]RULE _restore（）····双态双肽S ·[过渡]图三.ping-ped抽象机制。抽象是在增强的签名上进行的，其中，签名是“具体”语义的规范 对于这个特定的方程抽象的限制是，除了初始化ping阶段的结构规则之外，为抽象添加的所有方程都在Rcij中的项上。过程抽象的本质。这一步的想法是让局部变量保持在过程该算子在[16，17]中被描述为迭代算法，其读作：- 设σ是当前状态，σJ是来自过程调用点的状态- 设n是全局变量g1的个数。gn和σ0= σJ;- 对于1≤i≤n，执行以下if-then-else步骤：1. 如果σ（gi）=，则σi=σi−1[/gi]else2. 若σ（gi）=σ（gj），则对某个ji，有enσi=σi−1[σi−1（gj）/gi]else3. 若σ（gi）=σ（GJ），则对某个冻结变量GJ，nσi=σi−1[σJ（g）/gi]else108I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97JK：：= pingBagItem|ped地图规则平····gi−gnSnsigmai···retpedSn[结束结构]规则···Gi›→···sigma···Gi··gi−gn···Gi›→·⊥···[步骤1. 结构]规则···Gi→K Gj→K···ΣΣGi·Gsgi−gn···Gj···g1−gn···Gj›→KJGi›→王空军···当<$BoolGj在Gi Gs中时，[步骤2. 结构]规则<$Gi<$→Kfrz（G）<$→K Sσ <$···G<$→KJ···σ 1吉·Gsgi−gn<$GGGs g1−gn<$···Gi›→王空军···当<$BoolKinS[G GGs-SetGi Gs][步骤3. 结构]规则Gi›→K SsigmaGi·Gsgi−gn<$GG g1−gnSiSi[nextFreeValue（S（Gi），|值S|，S）/Gi]当<$BoolKinS[frzSet（GGs）]<$Bool<$BoolKinS[GGs-SetGi Gs]BoolKBool[步骤4 -5. 结构]图四、抽象过程的返回语句的结构规则4. 如果在σi−1中使用了除以外的所有下标，则σi=σi−1else5. σi=σi−1[k/gi]，其中k是y σ i − 1未使用的最小抽象地址。图4我们给出了这个算法在K.也就是说，其中，σi、σj、σi分别包含映射σ、σJ和σi。迭代被保存在包含全局变量的单元格gi−gn中，这些全局变量将被算法处理单元格frzg1−gn维护所有全局变量，冻结变量g表示为frz（g）。关于图中的算法的几个考虑4：通过gi-gn单元实现迭代处理第一条规则通过将结果发送给ped操作符来终结迭代步骤1之间的一致性5. 算法中I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97109Rep由规则属性反映。if-then-else级联通过匹配和条件实现。3.2SIL缺陷的分析有了SIL stecK的抽象语义，我们可以将别名分析作为第2.2节中介绍的收集语义的实例化。也就是说，我们描述了收集单元的内容和关系。收集 单元维护两个单元、标题 和别名，如下所示：⟨⟨⟨⟨K⟩k⟨Map⟩state⟩head∗⟩heads⟨⟨Map⟩state∗⟩aliases⟩collect. 头部单元包含由良基关系使用的信息，以停止由收集语义引起的穷举执行。在穷举执行结束时，aliases单元格包含所有必要的别名信息。因此，别名单元可以是-分析，无论是事后或事后，与查询，如kep=？别名分析q代表需求驱动回想一下，收集语义通过定点迭代执行穷举执行。因此，这种关系有助于认识到某些计算达到了它们不能对收集的结果作出更多贡献。因此，我们依赖于保证在下推系统中发现的重复堆栈模式，并使用关联匹配定义关系如下：• 是假的，即，当前考虑的计算轨迹⟨⟨PaXaXaY⟩k⟨S⟩state⟩tracedoes not contribute to the update当计算轨迹是先前收集的磁头的重复时，因此，图1中的第二规则被实例化为：规则 PaXaXaYkS状态跟踪·⟨⟨PaXaY⟩k⟨S⟩state⟩head• 当计算轨迹不是任何先前收集的磁头的重复时，因此，图中的第一个规则1读作：规则 的状态跟踪··⟨····南卡罗来纳州post（···⟨⟨PaK ⟩k ⟨S ⟩state ⟩head当PaK<$k <$S<$态∈/Hs请注意，出于效率原因，我们只在当前计算是过程调用时应用∈/rep测试，而在所有其他情况下，关系都被认为是真的。这种简化的原因是过程调用是SIL steck计算中无限性的唯一来源例3.1我们在图5中讨论SIL stecK程序的别名分析结果。由于空间限制，我们不详细介绍如何计算别名分析的演变。相反，我们只列出了前几个步骤，并解释了其中的原因。110I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97使用may和must在最终结果上加别名gvars：xlvars：y{main：：y：=new;（x：=y + x：=new）; flag;main; y：=x}图五. 一个简单的SIL steck程序主节点k_frz（x）→ k_x→ k_y → k_state_trace_k_heads_ k_aliases$y：=newa（x：=y+x：=new）;flag;main;y：=xarestore（frz（x）→x<$→y<$→）kn_frz（x）<$→ n_x <$$> → n_y <$<$→ n_y态n_迹⟨⟨⟨main ⟩ k ⟨ frz(x) →⊥ x →⊥ y →⊥⟩ state ⟩ head⟩ heads......这是什么？$（x：=y+x：=new）aBarestore（frz（x）<$→x<$→ y<$→）k<$frz（x）<$→ <$x<$→ <$y <$→0 π态π迹...其中B是flag;main;y：=x$x：=newaBarestore（frz（x）›→x›→y→）kfrz（x）→x→y›→0状态跟踪⟨⟨ x:= y a B a restore(frz(x)→⊥x →⊥ y ›→⊥)⟩k⟨ frz(x)→⊥x →⊥ y›→0⟩state⟩trace...$$标记main;y：=xarestore（frz（x）→ fixx<$$> →fixy<$<$→ fixkfixz（x）→fixx<$→0y<$→0 fixstatefixturetrace$mainay：=xarestore（frz（x）→x→y→）kfrz（x）›→x›→1y›→0statetrace恢复mainay：=xarestore（frz（x）<$→恢复x→恢复y→恢复）恢复k恢复frz（x）→恢复x<$→0y<$<$→0恢复状态恢复跟踪⟨⟨frz(x)›→⊥x›→0y›→0⟩stat e⟨frz(x)→⊥x›→1y›→0⟩stat e⟩aliases. . . $100.. .注意，在这个例子中，我们使用flag作为一个兴趣点来回答查询“程序中特定点的别名信息是什么？"。全局别名分析将对每个程序点使用多个标记在分支点，我们为每个轨迹分配一个唯一的水印（作为布尔序列），该水印以别名的形式传播到状态单元。因此，在分析结束时，我们可以推断执行路径。例如，直到分析结束，具有x：=new的分支将在别名单元格中产生状态：（a，1， 0）1，（1， 2， 0）11，（2， 1， 0）111，（1， 2， 0）1111，（2， 1， 0）11111（其中通过（a，b，c）i，derstand_frz（x）<$→ax<$→by <$<$→cn状态，而i是水印）。 必须查询别名x=？y_id_n限制此执行路径，并且对查询y发送“no”。同时，对may alias的相同查询标识收集的状态（0，0， 0）0并回答“yes” to the same4结论和今后的工作在本文中，我们提出了一种技术，用于定义K个抽象语义规范上的分析和验证简而言之，我们将收集语义应用于作为有限下推系统给出的K个定义。我们实例这种技术与别名分析的抽象语义的SIL stecK。我们计划将K收集语义技术应用于Shylock的抽象语义模型检查，这是SIL steck的对象字段扩展此外，我们计划研究和标准化一种K方法，用于定义抽象，即对“具体”语义的抽象解释已经为“真正的”编程语言定义了语义最后，我们要感谢[2]的合著者团队为这项工作创造了前提，感谢K框架和匹配逻辑团队不仅为这项工作而且为许多其他工作提出了挑战和方法，最后但并非最不重要的是感谢匿名评论者提供了详细和非常感谢的反馈。I.M. Asanovoa e/electronicNotesinTheoreticalComputerScience304（2014）97111引用[1] 再见，我。 M.，和你也一样M在K框架中的预指示Abstr动作下的编译Proc. WRLA，LNCS，6381（2010），123[2] 再 见 ， 我 。M. ，deBoer ， F. ， Bons an g ue ， M. ， Lucanu ， D. ，和 Rot ， J ，BoundedModelCheckingofRecursive Programs with Pointers in K，WRLA（2012），接受演示。[3] Bouajjani，A.，Esparza，J.，和Maler，O.，下推自动机的可达性分析：在模型检验中的应用，Proc.CONCUR，LNCS，1243，（1997），135[4] Cousot，P.，摘要解释，麻省理工学院课程16.399，（2005）。[5] Cousot，P.，和Cousot，R.，逻辑程序的抽象解释和应用，逻辑程序设计杂志，13（2[6] Eker，S.，Meseguer，J.，和Sridharanarayanan，A.，The Maude LTL Model E10，Proc. WRLA，ENTCS，71（2002），162[7] 埃里森角，澳-地 和R oRissu，G.，C语言的可执行规范语义及其应用. POPL，ACM，（2012），533[8] 希尔斯，M.， 和R oRissu，G.， AREWRRTA，Schloss Dagstuhl，（2010），151-160.[9] Meseguer，J.， 和R oRissu，G.，重写逻辑语义学专业，理论计算机科学373（2007），213-237.[10] Meseguer ， J. ， 和 R oRissu， G. ， TheRewritingLogicSemanticsPro ject ： aProgressReport ， FCT ，（2011），1[11] R oRissu，G.，埃里森角，澳-地 和S chulte，W.，匹配逻辑：一个替代应用程序到Hoare/Floyd逻辑，AMAST，（2010），142[12] 若水，G.，和斯贾特夫·贾内斯库，一 、匹配逻 辑重写：在实用和通用框架中统一操作和公理语义，技术报告http://hdl.handle.net/2142/28357，伊利诺伊大学，（2011）。[13] R oRissu，G.， 和S·阿夫塔内斯库，A，MatchingLogic：ANewProgramVerificationApproach，NIERICSE[14] R oRissu， G. ，和 Serba nuta， T. F. 、 AnOverviewoftheK SemanticFramework， JournalofLogicandAlgebraic Programming，79（6）（2010），397[15] R oRissu， G. ，和 Serba nuta， T. F. 、 K-Maude ： ARewritingBasedToolforSemanticsofP rog rammingLanguages，Proc. WRLA，LNCS，6381（2010），104-122.[16] Rot ， J. ， APushdown System Representation for Unbounded Object Creation ， InternalReporthttp://www.liacs.nl/assets/Masterscripties/10-06-JurriaanRot.pdf ，B.Sc.Thesis ， LeidenUniversity，（2010）.[17] Rot，J.，Bonsangue，M.，和de Boer，F.， 一个用于创建无界对象的下推自动机，FOVEOOS，（2010），接受演示。[18] 你别这样T. F.、Arusoaie，A.，LazZeliar，D.，埃里森角，澳-地Lucanu，D.， 和R oRissu，G.， K引物（版本2.5），在当前卷.[19] 你别这样T. F.、 R oRissu，G.， 和Meseguer，J.，操作语义学的重写应用207（2）（2009），305[20] 你别这样T. F.、 R oRissu，G.， 和Stefanescu，A.，K和匹配逻辑的概述在当前卷中。[21] 郑，X.， 和Rugi ndela，R.， Demand-driven AliasAnalysisforC，POPL，（2008），197-208.
