字节码到BoogiePL形式化翻译的理论计算机科学电子笔记

理论计算机科学电子笔记190（2007）35-50www.elsevier.com/locate/entcsBytecode到BoogiePL的形式化翻译HermannLehner1 和彼得·穆勒r 2瑞士苏黎世联邦理工学院摘要许多现代程序验证器将待验证的程序及其规范转换为简单的中间表示，然后在此表示上计算验证条件。使用中间语言提高了工具的互操作性，并简化了小型验证条件的计算。尽管转换成中间表示对于验证器的可靠性至关重要，但这一步骤尚未得到正式验证。 在本文中，我们形式化的翻译将Java字节码的一个小子集转换为类似于BoogiePL的命令式中间语言。我们证明了翻译的合理性，通过展示每个字节码方法，其BoogiePL翻译可以被验证，也可以在直接对字节码进行操作的逻辑中被验证保留字：程序验证，验证条件，中间语言，Java字节码，BoogiePL1引言许多现代程序验证器，如ESC/Java [10]，Boogie [2]，Krakatoa [12]和Caduceus[9]，都是通过两个步骤来验证程序的。首先，他们将程序和规范翻译成一种中间表示，如守护命令，BoogiePL [7]或Why语言[8]。在第二步中，他们计算中间表示的验证条件，并将其传递给理论证明器。使用中间语言可以提高工具的互操作性。例如，Krakatoa和Caduceus将Java和C代码翻译为Why语言，这允许它们共享Why后端。此外，简单的中间表示便于通过传递生成小的验证条件[11]。转换为中间表示对于程序验证器的可靠性至关重要。它必须确保中间程序的验证条件足够强，以保证原始程序的正确性1邮箱：hermann. inf.ethz.ch2peter. inf.ethz.ch1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.05936H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35程序;否则中间程序可以被验证，尽管原始程序是不正确的。尽管它的重要性，健全的，翻译成一个中间表示尚未正式验证。在本文中，我们形式化了Java字节码到中间语言BoogiePL的无类型版本的翻译，并通过证明中间程序的验证条件至少与原始程序的相应验证条件一样强来证明翻译的可靠我们的形式化和证明[6，14]覆盖了Java字节码的一个大子集。由于篇幅的限制，我们在本文中关注一个小的，但有趣的子集纲要本文的组织结构如下。秒2描述了字节码子集和直接对字节码进行操作的最弱前提演算。秒3介绍了BoogiePL，包括一个最弱的前提演算。翻译从字节码到BoogiePL的转换在Sec中定义。四、我们通过第二节中的一个例子来说明翻译。第五，在安全性方面。六、我们在SEC中回顾相关工作。7和第二节中的其他结论8 .第八条。2Java字节码在本节中，我们将描述本文其余部分中使用的字节码子集。我们还解释了规范是如何形式化的，并概述了字节码语言的最弱前提（wp）演算。2.1语言子集我们考虑一个包含类、接口、字段、动态绑定方法和异常的顺序Java字节码子集。为了简洁起见，我们只考虑一个非常小的指令集。然而，这个子集是有代表性的，因为它包含主要组的指令：' iload n '用于寄存器和操作数堆栈的操作，' ifgt Label '用于控制堆栈指令，' invokevirtual Method '和'irereturn'用于方法调用和返回，以及' new TypID '和' getfield FieldID '用于堆操作。大多数剩余指令的翻译类似于这些代表。标签、类型ID、方法和FieldID是标签、类和接口名称、方法名称和程序的字段名称的排序为了简单起见，我们假设类型名、方法名和字段名在程序中是唯一的。我们期望字节码程序的控制流程图是可约的，这意味着控制流程图中的每个循环只有一个入口点。Java编译器总是生成可约化的控制流图。对于手写的字节码，这个属性可以通过代码复制来实现。我们通过一个函数处理程序来建模异常表，该函数处理程序返回给定类型及其所有子类型的异常的所有可能处理程序包括子类型是必要的，因为执行的异常处理程序是基于异常对象的运行时类型动态确定的，该异常对象可以是静态已知类型的子类型。H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3537特殊标签处理程序：方法×标签×类型ID→标签集2.2状态模型字节码程序的执行状态由堆、操作数堆栈和寄存器中的值组成。排序Value对对象引用和基元类型（如整数）的值进行建模。对象的实例变量由排序InstVar建模。函数iv：Value×FieldID→InstVar为给定的对象和字段标识符生成实例变量。堆被建模为具有主排序Heap和以下操作的数据类型：更新：堆×InstVar×值→堆获取：堆×InstVar→价值alloc： Value× Heap→ bool添加：堆×类型ID→堆new：堆×TypID→值update（h，i，v）用值v更新堆h中的实例变量i。get（h，i）得到堆h中的实例变量i的值。对象创建由两个函数编码：new（h，C）在堆h中生成一个C类的新对象，add（h，C）生成扩展堆。堆模型的公理化将这两个函数联系起来，并确保这两个函数的使用一致。最后，alloc（v，h）给出值v是否在堆h中分配。我们省略了这些函数的公理化，因为我们的翻译和可靠性证明并不依赖于它。细节在一篇文章中由Poetzs ch-HeteranddMuüller[13]给出。在对JVM的状态建模时，我们区分了方法执行之前、期间和之后的状态。PreState包含堆和方法参数的值，LocalState包含堆，操作数堆栈以及方法参数和局部变量的值，PostState包含堆和值，如果方法正常终止，则值是方法的结果值，如果方法突然终止，则值是异常。PreState：（堆×参数）LocalState：（Heap×OperandStack×Locals）PostState：（Heap×Value）其中Arguments、Locals和OperandStack是Value的列表。2.3质量标准我们将字节码程序的规范形式化为一个规范表，它可以由以下函数访问38H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35前： 方法→（PreState→bool）post：Method→（PreState×PostState→bool）postX：Method →（PreState×PostState→bool）local：Method×Label→（PreState×LocalState→bool）pre（m）产生方法m的前提条件，它是PreState上的谓词。post（m）和postX（m）分别产生m的正规后置条件和例外后置条件。两者都是PreState（引用堆和方法参数的初始值）和PostState上的谓词。标签l处的局部注释由local（m，l）表示。它们是PreState和LocalState上的谓词。本地anno-站用于编码循环不变量。为了避免wp演算中的定点计算，我们要求控制流图中每个循环的入口点在指定表中有一个局部注释。local（m，l）是unfined，如果l不是循环的开始2.4字节码的直接验证条件生成我 们 对字节码的最 弱 的 前 置 条 件 演 算 是 Gr′egoire 演 算 的 简 化 版 本 ， 其 中hichisprovesondw。R. t. 非操作性电磁学[6]。 在这一小节中，我们介绍了本文其余部分所需的微积分部分。我们假设每个字节码程序在应用wp演算之前都通过了字节码验证器。因此，我们不证明类型的正确性和没有堆栈上和下的演算。我们定义一个函数wpvc：Method×Label→（PreState×LocalState→bool）。WPVc（m，l）产生方法m的标签l处的指令的最弱前提条件。如果这个最弱的前置条件成立，从l开始的执行将：（1）在满足m的错误，或（4）永远运行。为了处理本地注释，我们使用了第二个wp函数，它产生了本地前提条件。局部前提条件是指定表中的局部注释（如果有），否则是最弱的前提条件：.wpl（m，l）=local（m，l）：如果定义了local（m，l），wpvc（m，l）：否则最弱的预条件函数wpvc在图中定义。1.一、 对于iload n，wpvc将后继指令的本地前置条件应用于适配的本地状态。对于ifgt，wpvc产生可能的跳转目标和后继标签的局部先决条件的合取，通过适当的条件弱化irereturn最弱的前置条件是普通方法后置条件。 new类似于iload n。对于getfield，最弱的先决条件要求栈顶元素为非空，以防止NullPointerException。 对于方法调用，我们必须证明目标是非空的，前提条件是满足的。H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3539在L负荷;负载国际新闻集团返回新测试wpvc（m，l）（σ0，（h，top：：os，reg））=wpl（m，l+1）（σ0，（h，reg[n]：：top：：os，reg））（top>0wpl（m，lJ）（σ0，（h，os，reg））（top≤0<$wpl（m，l+1）（σ0，（h，os，reg）立柱（m）（σ0，（h，顶部））wpl（m，l+1）（σ0，（add（h，t），new（h，t）：：top：：os，reg））getfieldf顶部null{\displaystyle\null}} wpl（m，l+1）（σ0，（h，get（h，iv（top，f））：：os，reg））invokevirtualttop/=nullpre（t）（h，top）JiangJIANG，rv：（post（t）（（h，par），（hJ，rv））后wpl（m，l+1）（σ0，（hJ，rv：：os，reg））（postX（t）（（h，par），（hJ，rv））wp（m，l）（σ，（hJ，rv，reg））li0li∈handdlers（m，l，typeof（rv）））其中，par是表示tFig. 1.字节码的最弱前提演算。标签l+1表示标签l的文本后继者。 函数typeof产生一个值的运行时类型后置条件的处理必须考虑正常终止和突然终止。也就是说，正常方法后置条件必须隐含后继指令的局部前置条件，而异常方法后置条件必须隐含所有可能的异常处理程序的局部前置条件。注意如果异常可能被传播，则处理程序的值包括NULL。因此，我们定义wpvc（m，m）=postX（m）。注意，这个最弱的前提条件演算强制指令不抛出运行时异常。例如，getfield要求接收器为非空值.这个要求是不完整性的来源：一个解引用null的方法可能会捕获NullPointerException并仍然满足其规范，但不能在我们的wp演算中验证。然而，防止运行时异常通过避免可能引发运行时异常的为了验证方法m，必须证明（1）方法前提条件隐含第一条指令的局部前提条件，以及（2）对于每个具有局部注释的标签，局部前提条件wpl（m，l）隐含最弱的前提条件wpvc（m，l）。后一项义务是为了表明循环不变量实际上得到了40H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）353BoogiePL在本节中，我们简要概述了BoogiePL并介绍了一个wp演算。有关详细信息，我们参考DeLine和Leino的报告[7]。 专注于本质 在字节码翻译中，我们使用了一个无类型的BoogiePL版本。然而，我们的完全形式化[6]适用于类型化语言。3.1概述和状态模型BoogiePL程序由一个前奏和一个程序列表组成。序言具体说明了一阶逻辑中使用全局变量、常量、公理和未解释函数的背景理论。程序包含规范和实现。在我们的翻译中，我们不使用程序规范。过程的实现从声明所有局部变量开始，然后是一个或多个一个块有一个唯一的ID，一个由BoogiePL命令组成的主体，并以一个非确定性的goto结束，它指定了所有控制流程图中的可能后继块一个空列表的goto块ID终止执行。 BoogiePL提供了以下命令：赋值、调用、假设、断言和破坏。havage命令将任意值赋给给定变量。在下文中，我们将对过程名重用sortMethodBoogiePL程序的状态由所有全局和局部变量的值组成。排序Valuebpl包含BoogiePL程序的所有可能值：状态bpl：Var›→Valuebpl3.2BoogiePL验证条件生成我们对BoogiePL的wp-演算与Barnett和Leino的类似[3]。然而，它要求BoogiePL程序的控制流程图是非循环的，而Boogie工具接受循环控制流程图并将其内部转换为非循环图。我们在翻译中明确了这种转换，见第四点三我们假设BoogiePL方法的命令是编号的。我们使用术语position而不是label来表示BoogiePL命令的编号，以避免与字节码指令的标签混淆BoogiePL的最弱预处理函数wpbpl：Method×Position→（Statebpl→bool如果过程m中位置pos的最弱前提成立，则从pos不会由于断言冲突而中止。也就是说，程序将终止或永远运行。最弱的预条件函数wpbpl在图中定义。二、4从Bytecode到BoogiePL的在本节中，我们将描述如何将字节码子集转换为BoogiePL。H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3541位置命令假设P断言P x：=e大破坏xgotopos 1，... ，位置nwpbpl（m，pos）=Pwpbpl（m，pos+1）Pwpbpl（m，pos+1）wpbpl（m，pos+1）[e/x]BPL（m，pos+1）wpbpl（m，位置i）i：=1..n图二. BoogiePL的最弱前提演算。用项e替换变量x表示为[e/x]。4.1关于Bytecode Program的信息我们的翻译使用字节码验证器计算的信息，即(1)每个标签处的操作数堆栈的高度，以及（2）每个方法的控制流程图。我们通过以下函数对这些信息进行sh：方法×标签→intisEdge：Method×Label×Label→boolisEdgeTarget：方法×标签→boolisBackEdge ： 方 法 × 标签×标签→bool isBackEdge目标：方法×标签 →boolsh（m，l）在执行方法m的标签l处的指令之前产生操作数栈的顶部元素的索引。如果在方法m的控制流图中存在从标签l1到标签l2的边，则isEdge（m，l1，l2）产生真。 如果是这种情况，isEdgeTarget （ m ， l2） 产生 true。 函数 isBackEdge 和isBackEdgeTarget类似于isEdge和isEdgeTarget，但仅考虑控制流程图中的后向边。4.2BoogiePL中字节码状态的编码我们通过一些BoogiePL变量对字节码程序的状态进行Prestate：第二节中描述的堆模型。2被编码在BoogiePL程序的前奏中。我们在这里不显示这种形式化，因为它并不有趣。我们使用变量old heap来引用prestate的堆字节码方法的n个参数由BoogiePL过程的参数parami（i = 0，.，n−1）。本地状态：我们使用全局变量heap来建模当前执行状态的堆。操作数堆栈由变量堆栈i建模，其中i表示堆栈的高度（从0开始）。寄存器（表示局部变量和参数）由变量regi建模。由于类文件中给出了操作数堆栈的最大高度和使用的寄存器数量，因此我们静态地知道必须声明多少个堆栈i和寄存器i 在BoogiePL程序中。42H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35我们使用以下缩写：params表示变量列表parami，stacks表示所有堆栈元素stacki，而req表示所有寄存器regi。一个字节码程序的状态和它的翻译形式上是通过映射函数map：Method×Statebpl×Int→（PreState×LocalState）：map（m，ρ，h）=.- 是的Σρ（旧堆），ρ（参数），ρ（堆），ρ（栈h），. ，ρ（stack0），ρ（stack0）4.3后边缘消除正如SEC所解释的那样。2.4，我们的平移消除了控制流图中的后向边，以避免wp演算中的定点计算重要的是要理解，后沿不仅发生在跳跃指令中。从指令到其文本后继指令的任何转换都可能是后沿。例如，在图3中的字节码程序中从标签8到标签11的转换是后沿，因为之前由于处理标签2处的跳转而访问过标签11。沿后边缘的过渡始终闭合控制流程图中的循环因此，我们可以假设后边缘的目标具有循环不变量的局部注释 在转换中，我们消除了后边缘，而是生成一个循环不变式保持的断言。一个forward-edge被简单地翻译成一个goto。这是由翻译功能TrEdge完成的。它被定义为可能的后继标签的列表。TrEdge[[m：方法，l：标签，ls：标签列表]]=#foreachlJ inls#ifisBackEdgeTarget（m，lJ）assertTrSpec[[local（m，lJ），（oldheap，params），（heap，stacks，params）]]#end if#end foreach#let l 1，.，l n= ls中的所有lJ，其中，<$isBackEdge（m，l，lJ）goto块11，.. . ，块1 n;在我们的符号中，打字机字体的文本直接打印，而斜体文本则由翻译器解释。以“#”字符开头的行描述代码是如何生成的。TrSpec将字节码规范转换为相应的BoogiePL表达式，从而替换堆，操作数堆栈，并通过给定的变量进行注册 我们使用的惯例是，从标签l开始的字节码基本块的BoogiePL块具有ID块l。4.4字节码指令函数TrInstr翻译单个字节码指令。PredictionAt（m，l）表示方法m中标记l处的指令。TrInstr[[m：M ethod，l：Label]]= #letcntr =sh（m，.ΣH. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3543l）44H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35#switchparametionAt（m，l）我们在下面介绍了开关的各个案例：加载：从寄存器中加载一个值被转换为对栈顶元素的栈变量的赋值。#caseloadnstackcntr+1：= regn;ifgt：分支指令被转换为非确定性的转到两个假定分支条件分别为真或假的处理器块。然后，真块跳转到目标标签 LJ。为了消除后边缘，我们在这一点上应用TrEdge。假块继续翻译下一个指导。#caseifgtlJgoto blocklTrue，blocklFalse;blocklTrue：假设堆栈cntr>0;TrEdge（m，l，[lJ]）blockl假：假设<$（堆栈cntr>0）;return：return指令将栈顶元素复制到栈底，然后跳转到特殊的块post，它断言当前方法#case return堆栈0：=堆栈cntr;goto post;new：对象创建被转换为BoogiePL版本的堆函数add和new的应用程序。#casenewtheap：= add（heap，t）;stackcntr+1：= new（heap，t）;getfield：在读取字段之前，我们断言栈顶元素（接收者）不为空。接下来，栈顶元素被当前堆中field的值替换。#casegetfieldfassert stackcntr/=null;堆栈cntr：= get（heap，instvar（堆栈cntr，f））;invokevirtual：我们使用变量pre heap和arg0来保存堆的旧值和调用的接收者，因为它们可以在被调用方方法的后置条件中使用。我们保存接收器，但不保存其他参数，因为H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3545接收器的堆栈位置将被方法结果覆盖，而其他参数被保留。P表示被调用方方法的（隐式和显式）参数的数量。实际的方法调用翻译如下：我们断言接收者不为被调用方可能的副作用通过调用堆来解决。由于被调用方可能正常终止，也可能突然终止，因此我们继续使用不确定的goto。对于突然终止，我们擦除关于堆栈0的所有信息，堆栈0现在包含：获取异常对象。为了简单起见，我们在这里不考虑被调用方的throws子句，而是简单地假设异常是Throwable类型的分配对象（typeof产生值的运行时类型，<：表示子类型关系）。然后我们假设被调用方的异常后置条件，并跳转到异常的所有可能处理程序使用throws子句更细粒度地处理异常是很简单的。对于正常终止，我们擦除所有关于包含接收器的堆栈位置的信息，因为这个位置现在将包含方法结果。然后我们假设被调用者的正常后置条件。在翻译中，我们使用args来引用调用的参数，即，args=[arg0 ， stackcntr−P+2 ， . ，stackcntr] 。#caseinvokevirtual 被调用方arg0：= stackcntr−P+1;pre-heap：= heap;int arg0/=null;assertTrSpec[[pre（callee），（preheap，args）]]大破坏堆;gotoblockl正常，blockl异常;blockl例外：havocstack0;assumealloc（stack0，heap）函数typeof（stack0）<：Throwable;assumeTrSpec[[postX（callee），（pre heap，args），（heap，stack0）]]TrEdge（m，l，handlers（m，l，Throwable））块l正常：#letres =stackcntr−P+1浩劫;假设TrSpec[[post（callee），（preheap，args），（heap，res）]]4.5指令序列TrInstSeq[[m，l]翻译从标签l开始直到方法m结束的指令序列。它使用m的控制流程图来确定l是否是基本块的开始。 如果l是后边缘的目标，我们知道l是循环的入口我们应用Barnett和Leino [3]描述的策略46H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35使循环体表示一般循环迭代。这是通过调用所有可能被循环修改的变量（堆，操作数堆栈和寄存器，但不是堆的预状态值和参数）并假设循环不变来实现的。然后我们翻译标签l处的指令。如果从l到其文本后继l+1的转换是控制流图中的边，则我们必须结束当前块，并且可能使用TrEdge应用后边缘消除。最后，我们继续翻译指令序列的其余部分TrInstSeq[[m：M ethod，l：Label]]=#ifisEdgeTarget（m，l）区块l：#ifisBackEdgeTarget（m，l）havavage heap，stacks，havage heap;assumeTrSpec[[local（m，l），（oldheap，params），（heap，stacks，params）]]#end if#end ifTrInstr[[m，l]]#ifisEdge（m，l，l+1）TrEdge（m，l，[l+1]）#end ifTrInstSeq[[m，l+1]]4.6方法翻译方法的翻译是通过函数Tr[[m：Method]完成的。该函数生成BoogiePL过程的签名，声明局部变量，并将转换函数TrBody应用于方法体，我们将在下面描述。方法体的转换从创建一个块init开始，它保存了预状态的堆，以便以后在本地注释和后置条件中使用。此外，它还将参数的值复制到寄存器变量中。P表示方法的（隐式和显式）参数的数量接下来，我们假设的前提条件。如果方法体的第一条指令是跳转目标，我们断言局部注释（如果有的话），并通过跳转到第一条指令开始的块来结束这个块。方法体的指令使用TrInstSeq进行翻译。TrBody还为方法的正常和异常后置条件生成块TrBody[[m：M方法]]=初始化：heap：= heap;#for i：= 0. （P-1）：regi：= parami;#结束assumeTrSpec[[pre（m），（oldheap，params）]];H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3547#ifisEdgeTarget（m）#ifisBackEdgeTarget（m）assertTrSpec[[local（m，0），（oldheap，params），（heap，params，params）]] #end ifgoto block 0;#end ifTrInstSeq[[m，0]]职务：assertTrSpec[[post（m），（old heap，params），（heap，stack0）]];goto;X后assertTrSpec[[postX（m），（old heap，params），（heap，stack0）]];goto;5例如我们用两次方法来说明我们的翻译。图3显示了该方法的源代码、字节码和规范表。图4示出了平移的结果。这些规范包括在假设和断言命令中。请注意，从标签8到11的后边缘在平移期间被消除相反，块11通过具有状态并假设循环不变来开始。我们在Boogie中验证了这个示例的类型版本6健全性在这一节中，我们提出一个可靠性定理，并简述主要引理的证明。完整的证据在我们的报告中提供[6，附录E]。定理6.1设m是指定字节码程序的方法。如果m到BoogiePL的转换可以在BoogiePL的wp演算中验证，那么m也可以在直接对字节码进行操作的演算中验证这个定理是下列引理的推论。引理6.2设m是指定字节码程序的方法，l是m中的标号。m在对应于标签l的位置处的BoogiePL平移的最弱前提条件暗示m在标签l处的最弱前提条件m，l，ρ：（wpbpl（Tr（m），其中，Ruppos（Tr（m），l）产生TrInstr（Tr（m），l）的第一个BoogiePL命令的位置。证明：证明通过归纳在字节码方法m的控制流程图上运行，更准确地说，是在标签l到方法末尾的距离上运行48H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35假设param 0> 0;//需要//@需要x> 0;//@确保\result==\old（x）+\old（x）;publicintfindDuplicate（intfindDuplicate）{inti= x;//@循环不变式//@x + i ==\old（x）+\old（x）<$i ≥ 0;while（i> 0）{x++; i−−;}返回x;}第0章：加载0一曰：iStore 1第二章：goto11第五章：国际工业公司0、1个第八章：国际工业公司一，一11：iload 112：ifgt515：iload 0第16章：返回规格表：预（两次）（h0，[p0]） ≡均p0>0post（twice）（h0，[p0]）（h，rv）rv=p0+p0local（twice， 11）（h0，[p0]）（h，[s0]，[r1：：r0]）r0+r1=p0+p0<$r1≥0图三. 带注释的Java程序和相应的带有规范表的implementationtwice（param0）return（result）{varstack0，reg0，reg1，old heap;初始化：旧堆：=堆; reg 0：=param 0;stack0：= reg0;int n = stack0;//0：including//1：iStore 1assertreg 0 + reg 1 == param 0 + param 0表示 reg 1≥ 0;//循环不变式goto块11;//2：goto11第五块：reg0：= reg0 + 1;reg1：= reg1− 1;//5：inc 0，1//8：iinc 1，1返回;块11：havastack0，reg0，reg1;assertreg 0 + reg 1 == param 0 + param 0表示 reg 1≥ 0;//循环不变式假设reg 0 + reg 1 == param 0 + param 0 <$reg1≥0;//循环不变式stack0：= reg1;gotoblock 12 true，block 12 false;// 11：负荷1//12：ifgt 5块12真：假设stack 0> 0;goto块5;块12假：假设！（stack0>0）;goto块15;第15块：stack0：= reg0;result：= stack0;gotopost;职务：// 15：加载0// 16：return返回;}断言结果== param 0 + param 0;//确保见图4。 BoogiePL翻译的例子与突出显示的注释部分。H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3549不考虑后边缘。 基本情况涵盖了终止方法的所有指令，特别是irereturn。所有其他说明均包含在诱导步骤中。在下文中，我们示出了归纳步骤的一种情况，即标签l处的指令是iloadn的情况。根据TrInstSeq（m，l）的定义，我们必须考虑指令翻译的三个部分：（1）如果至少有一个后边缘指向l，则局部状态被破坏，并假设循环不变量。(2)指令iloadn本身被翻译。(3)根据控制流程图，指令的BoogiePL代码后面是一个suprix。根据定义，bypos产生部分（2）的第一个位置。 Part（1）需要 以显示循环不变式产生的证明义务（见第二节的最后一段）。2.4），但与此引理无关。因此，我们在下面考虑TrInstr（Tr（m），l）的输出。我们从展开左边的含义开始：wpbpl（Tr（m），bppos（Tr（m），l））（ρ）wpbpl（Tr（m），bippos（Tr（m），l）+1）[regn/stackcntr+1]（ρ）wpbpl（Tr（m），puppos（Tr（m），l）+1）（ρ[stackcntr+1→ρ（regn）]）对于第（3）部分，我们必须考虑四种情况：（a）存在从l到l+1;（b）存在从l到l+1的前向边缘，并且存在至少一个指向l+1的后向边缘;（c）存在从l到l+1的前向边缘，但是l+1不是后向边缘的目标;（d）从l到l+1的过渡不是控制流图中的边缘，即，两个标签属于相同的基本块。我们继续区分情况。情 况 （ a ） ： 翻 译 断 言 循 环 不 变 式 并 返 回 。 下 面 我 们 用 ρJ 表 示ρ[stackcntr+1<$→ρ（regn）]。通过TrEdge的定义，我们得到：wpbpl（Tr（m），bppos（Tr（m），l）+1）（ρJ）local（m，l+1）（map（m，ρJ，sh（m，l+1）wpl（m，l+1）（map（m，ρJ，sh（m，l+1）wpvc（m，l）（map（m，ρ，sh（m，l）情况（b）：转换断言循环不变量并跳转到下一条指令。所以我们得到：wpbpl（Tr（m），bppos（Tr（m），l）+1）（ρJ）local（m，l+1）（map（m，ρJ，sh（m，l+1）{bpl（Tr（m），pos（Tr（m），l+1））（ρJ）其中pos（Tr（m），l+1）是TrInstSeq（m，l+1）的第一个命令的位置由于wpvc处理情况（b）与情况（a）完全一样，上述合取意味着wpvc（m，l）（map（m，ρ，sh（m，l）。情况（c）：转换在位置gotopos（Tr（m），l）+1处生成命令goto pos（Tr（m），l+1）因此，我们有：wpbpl（Tr（m），bppos（Tr（m），l）+1）（ρJ）wpbpl（Tr（m），pos（Tr（m），l+1））（ρJ）50H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）35由于l+1不是后边缘的目标，pos（Tr（m），l+1）与pmpos（Tr（m），l+1）的位置相同，我们可以应用归纳假设：wpbpl（Tr（m），pos（Tr（m），l+1））（ρJ）=πwpvc（m，l+1）（map（m，ρJ，sh（m，l+1）wpl（m，l+1）（map（m，ρJ，sh（m，l+1）wpvc（m，l）（map（m，ρ，sh（m，l）情况（d）：这种情况在指令翻译之后不生成任何suprix。因此，我们有pos（Tr（m），l+1）=1/ pos（Tr（m），l）+1。这一情况的其余部分类似于情况（c）。Q7相关工作ESC/Java [10]使用保护命令作为中间表示。Kraka- toa [12]和Caduceus [9]都将程序翻译成Why语言。据我们所知，这些翻译都没有正式化和验证。我们希望我们的工作能够适应这些翻译，尽管处理源程序而不是字节码将需要改变技术细节。Boogie验证器[2]将带注释的CIL代码转换为BoogiePL。这种转换的某些我们的形式化和证明涵盖了更大的语言子集，特别是异常，这是尚未处理的布吉。Barnett和Leino [3]提出了BoogiePL的一个Passification并证明了合理性。结合我们的结果，这表明字节码到被动BoogiePL的转换是合理的。Our wp-calculusforytecodeisinspirdbyGr′egoire[6]. 我们的形式化可以很容易地适用于其他字节码逻辑[1，4，5]8结论我们已经正式翻译的一个小子集的Java字节码BoogiePL和证明这种翻译的合理性。这项工作填补了几个程序验证器的合理性论证中的空白。我们通过使用相同的堆模型和字节码和BoogiePL转换的非常相似的状态模型，设法保持翻译和证明的复杂性此外，我们的翻译依赖于字节码验证器提供的保证和信息作为未来的工作，我们计划扩展翻译，以涵盖整个Java字节码指令集。一个更长远的目标是使用从字节码到BoogiePL的转换作为Proof-Carrying Code架构的一部分，这将使正式的可靠性证明变得更加重要。致谢。这项工作的部分资金来自欧盟委员会信息社会技术计划，IST-2005-015905MOBIUS项目下的未来和新兴技术。H. Lehner，P.Müller/Electronic Notes in Theoretical Computer Science 190（2007）3551引用[1] F. Y. B和NWART和P。 Müller. Apro gra