字节码程序逻辑验证的Hoare风格逻辑及其应用

理论计算机科学电子笔记141（2005）255-273www.elsevier.com/locate/entcs字节码的程序逻辑FabianBannwarrt1和PeteterMuüll er2，3ETHZürich，CH-8092Zürich，Switzerlandd摘要字节码语言（如Java字节码或.NET CIL）的程序逻辑可用于将证明携带代码概念应用于字节码程序，并验证字节码程序的正确性属性。本文提出了一种类似于Java字节码和CIL的顺序字节码内核语言的Hoare风格逻辑。该逻辑处理面向对象的特性，如继承、动态方法绑定、具有破坏性更新的对象结构，以及具有跳转的非结构化控制流。它是健全和完整的。关键词：Java字节码，.NET CIL，程序验证，Hoare逻辑1介绍中间语言（如Java字节码和.NET CIL）是标准化执行环境的一部分，独立于特定的硬件、操作系统或源编程语言。因此，它们支持平台独立性和语言互操作性。虽然程序通常是用源语言开发的，然后编译成中间语言（字节码），但有几个应用程序要求在字节码级别而不是源代码级别上应用形式推理：（1）用于小型设备的软件通常直接用中间语言开发，这种软件通常具有很高的正确性和安全性要求，可以通过应用于字节码级别的形式验证来满足。（2）第十五条第一款：第1fybannwart@student.ethz.ch2peter. inf.ethz.ch3这项工作得到了ETH Research Grant TH-26/04 -2的支持1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.026256F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255将程序属性的证明转换为编译代码，例如字节码。代码消费者可以在执行来自不可信源的代码之前检查这些证明(3)关于字节码程序的证明可以用来改进和加速JIT编译[21]。字节码程序的形式验证需要字节码的程序逻辑本文提出了一种用于内核字节码语言的Hoare风格的程序逻辑。该逻辑支持典型的面向对象特性，如类和对象、继承、实例字段、实例方法和动态方法绑定，以及具有条件和无条件跳转的非结构化控制流。为简洁起见，本文省略了静态类成员、例外处理、类初始化和值类。然而，我们的逻辑涵盖了这些特征[4]。将我们的逻辑扩展到完整的Java字节码或.NET CIL非常简单。Approach. 本文中介绍的逻辑是在一个项目中开发的，该项目旨在从经过验证的源程序自动生成经过验证的字节码。也就是说，我们的目标是开发一个所谓的证明转换编译器，它将源程序和源程序的某些属性的证明转换到字节码级别[3]。证明转换编译器类似于证明携带代码中的证明编译器[8]，但需要源证明作为输入。为了简化证明翻译，我们的字节码逻辑保留了Poetzsch-HelouteranddMuüllers我们的字节码逻辑[ 1 9 ]：两种逻辑都基于相同的对象存储模型，以相同的方式处理继承，动态方法绑定和递归，并使用相同的语言无关规则（例如，结果规则）。因此，相应的源代码和字节码程序的证明具有类似的证明结构，并且基于一阶逻辑中相同的证明义务（例如，对于结果规则）。对于字节码指令，我们为具有非结构化控制流的程序调整程序逻辑[5]。与经典Hoare逻辑中使用的三元组不同，每条指令I之前都有一个断言，该断言给出了代码中必须在该点保持的所有属性，以便能够整体验证给定的方法体这个前提条件必须由I的所有前置指令建立，这通常包括程序文本中位于I之前的指令以及跳转到I的所有指令。我们的逻辑假设字节码程序是格式良好的，特别是类型良好的。也就是说，我们考虑字节码验证器接受的程序。纲要我们介绍了字节码的核心语言和它的操作语义。二、程序逻辑见第2节。3 .第三章。我们勾勒出F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255257在SEC中的可靠性证明四、节中5，我们展示了我们的逻辑如何以WP方式应用相关工作在SEC中讨论。六、2字节码语言VMK在本节中，我们介绍字节码内核语言VMK及其操作语义。2.1VMK程序与Java或.NET一样，VMK程序由带有字段和方法的类组成。这些方法被实现为由一系列带标签的字节码指令组成的方法体。字节码指令在计算堆栈（有时称为操作数堆栈），局部变量（也包括参数）和对象存储（堆）。VMK的指令连同它们的操作语义一起解释为了保持形式简单，我们做了一些假设：方法总是虚的，返回一个值，并接受两个参数：接收者this和一个显式参数p。每个方法体都以一个返回指令结束，该指令将控件返回给调用方。此指令只能作为方法体的最后一条指令出现。方法返回存储在特殊局部变量result中的值。在本文中，我们省略了静态类成员、异常、类初始化和值类。我们的技术报告[4]中提供了这些功能的逻辑扩展和此处未讨论的VMK与Java字节码和.NET CIL非常相似。但是，它不支持CIL这些特性可以通过代码扩展来处理[23]。此外，VMK不支持CIL.beforefieldinit，表示类可以在访问静态字段之前的任何时间初始化（也就是说，不一定要在类的第一次使用这种行为很难在程序逻辑中建模2.2对象存储库源程序和字节码程序支持对对象存储的相同操作。因此，我们建立在对象存储的现有形式模型[18]上，我们在这里简要总结。所有对象的状态以及当前程序状态中是否分配了某个对象的信息通过一个带排序的抽象数据类型形式化258F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255ObjectStore和以下函数：iv（v，f）：V值×F ieldId→InstV ar操作系统配置a：=v：ObjectStore×InstV ar×Value→ObjectStore操作系统（f）：ObjectStore×InstVar→V alue操作系统配置：ObjectStore×ClassTypeId→ObjectStorenew（OS，T）：ObjectStore×ClassTypeId→值一个值是一个原始类型或引用的值Field Id和ClassTypeId分别是字段和类的唯一标识符。InstVar是程序中所有对象的字段地址的集合。iv（v，f）从对象v得到一个由f标识的场的地址。OSa：=v返回对象存储，其中实例变量a被更新为新值v。OST产生存储区，其中分配了类型T的新对象。 new（OS，T）返回OS中T类型的新对象。关于这些函数的公理化，请参见[18]。为了在形式语义中统一处理变量和对象存储，我们使用$作为当前对象存储的标识符2.3操作语义在本小节中，我们提出了VMK的操作语义。配置。一个方法执行的配置函数S，σ，l由一个状态S、一个计算栈σ和程序计数器l组成，l是下一个要执行的指令的标签。状态将局部变量的标识符（sortV arId）、形式参数和当前对象存储映射到值。计算堆栈是一个值序列。状态（V arId{this，p} →Vvalue {undef}）×（{$} →ObjectStore）堆栈堆栈值对于S∈State，我们将应用程序的S（x）写入变量或参数-对象存储的应用程序的ter identifier和S（$）。 序列（σ，e1，e2，. . ）是从σ通过附加e1，然后e2等获得的序列。l是有效标签，即，它在标签集合{0，.、|p|方法主体p的{\displaystylep}。|p|表示p中的指令数。p（l）是p中标签l处的指令。当方法体p从上下文中清除时，我们简单地将标签l处的指令写入I l。指令语义学转移关系p;S，σ，l→SJ，σJ，lJ表示在方法体p中执行指令Il带来F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255259[……l：pushcv.. . ];S，σ，l→S，（σ，v），l+1[……l：pushvx.. . ];<$S，σ，l<$→ <$S，（σ，S（x）），l+1<$[…… l：pop x.. . ];<$S，（σ，v），l<$→ <$S[x<$→v]，σ，l+ 1<$[…… l：binopop op.. . ];S，（σ，v1，v2），l→S，（σ，v1opv2），l+1[……l：brtruel′.. . ];S，（σ，true），l→ S，σ，l′[……l：brtruel′.. . ];S，（σ，false），l→ S，σ，l+1[……l：gotol′.. . ];S，σ，l→ S，σ，l′[……l：newobjT.. . ];<$S，σ，l<$→ <$ S [$<$$> →S（$）<$T<$]，（σ，new（S（$），T）），l+1<$τ（v）≤T[…… l：checkcast T.. . ];S，（σ，v），l→S，（σ，v），l+1y零[…… l：getfield T @ a.. . ];<$S，（σ，y），l<$→ <$S，（σ，S（$）（iv（y，T@a），l+ 1< $y零Sp=S[$<$→S（$）<$iv（y，T@a）：=v<$][……l：putfieldT @ a.. . ];S，（σ，y，v），l→Sp，σ，l+1y零p′=body（impl（τ（y），m））p′（l′）=returnp′;<${this<$→y，p<$→v，$<$→S（$）}，（），0<$→<$S′，σ′，l′<$Sp=S[$<$→S′（$）]σp=（σ，S′（结果））[…… l：invokevirtual T：m.. . ];S，（σ，y，v），l→Sp，σp，l+1Fig. 1. 操作语义学的规则。机器从配置到配置。对于给定的方法体，p，多步关系→p是→的自反传递闭包。转移关系是满足图中规则的最小关系1.一、指令pushc和pushv分别将常量和变量推入计算堆栈。也就是说，它们保持状态不变，向堆栈添加新值，并递增程序计数器。pop从计算堆栈中弹出一个值并将其分配给一个变量。我们通过指令binopop总结了所有的二元运算符，如布尔运算符和算术运算符，它从堆栈中弹出两个值，执行二元运算，并推动结果。条件和无条件跳转表示为：brtrue和goto，分别为newobjT创建类T的新对象，从而修改当前对象存储。将对新对象的引用推送到堆栈上。checkcastT指令执行强制转换的运行时检查。如果从堆栈顶部引用的对象v是T的实例，则程序计数器递增。否则，停止执行。在检查转换规则中，τ（v）是值v的（动态）类型，≤表示子类型关系。getfield和putfield读取和更新实例字段。这两条指令都弹出接收器对象y。 如果y为null，则执行260F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255停止。否则，getfield将实例变量的值压入堆栈。putfield弹出第二个值并 使 用 该 值 更 新 实 例 变 量 ， 即 修 改 对 象 存 储 。 字 段 标 识 符 写 为Type@fieldname。最复杂的规则处理虚方法的调用。我们认为方法调用是由它们的接收器表达式的静态类型扩充的.例如，在静态类型T的表达式上调用的方法m由T：m表示。方法T：m在类S中的实现用impl（S，T：m）或简单地用impl（S，m）表示。注意，S可以从超类继承m。方法m的主体用body（m）表示。invokevirtualT：m弹出接收方对象y和实际参数价值，v. 每个方法的执行都有自己的计算堆栈，它是由当它的方法调用完成时，因此，动态绑定方法m，p，J的主体是在一个空堆栈的配置中执行的，实际参数被分配给形式参数。pJ的执行在到达其最后一条指令return时终止。在将result的值推送到堆栈上之后，控件返回调用方。3程序逻辑本节介绍的霍尔风格的程序逻辑允许我们正式验证实现是否满足作为前置条件和后置条件给出的接口规范。3.1方法和指令规范我们对方法流的处理是针对Java源程序的Poetz sch-Heater和Mul？ler的程序逻辑[ 19 ]：我们区分方法实现和虚方法。方法实现T@m表示方法m在类T中的具体实现。一个虚方法T：m表示所有方法实现的公共属性，当m在静态类型T的接收器上被调用时，这些方法实现可能被动态调用，即impl（T，m）（如果T：m不是抽象的）和所有覆盖的子类方法。方法质量标准。方法和方法体的性质由形式为{P}comp{Q}的霍尔三元组表示，其中P，Q是排序的一阶公式，comp是方法实现T@m，虚拟方法T：m或方法体p。三元组{P}comp{Q}表示以下细化的部分正确性属性：如果comp的执行在满足P的状态中开始，则（1）compF. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255261L终止于Q保持的状态，或者（2）由于超出编程语言语义的错误或动作（例如，存储器分配问题）而导致comp中止，或者（3）comp永远运行方法规范的前置条件和后置条件不能引用变量或堆栈元素。前置条件可以引用形式参数this和p，以及当前对象存储$。后置条件可以指$和结果。对于递归方法的处理，我们使用形式为A {P}comp{Q}的序列，其中A是一组方法规范。直观地说，这样的证明表达了这样一个事实，即三元组{P}comp{Q}可以基于关于方法的一些假设A来证明（详见[19]）。指令规范。字节码程序的非结构化控制流使得处理指令序列变得困难，因为跳转可以将控制转移到序列中间或从序列中间转移。因此，我们的逻辑单独地处理每个指令：方法体p中的每个单独的指令I1具有前提条件E1。一条带有前置条件的指令被称为指令规范，写为{El}l：Il。显然，指令规范{El}l：Il的含义不能孤立地定义。{E1}1：I1表示如果在程序代码为位置1时前提条件E1成立，则I1的后继指令Ij的前提条件E1J在I1正常终止后成立。与方法规范一样，指令规范也可以具有约束力，选项。假设集合A的指令规范表示为A.I.I.I.连接说明和方法规范。单个指令可以在方法体级别上组合，因为VMK保证构成方法体的指令序列总是在第一条指令处进入，并在最后一条指令之后离开。 所有的跳跃都是低-在方法体中调用。方法实现的前提条件是其主体的第一条指令的前提条件，方法后条件是返回指令的前提条件。因此，一个方法实现T@m满足它的方法规范，如果所有指令都在T@m的主体满足它们的指令规范。这种联系由body规则形式化：{0，.、|体（T @ m）|− 1}：（A <${Ei}i：Ii）A{E0}体（T@m）.ΣE|体（T@m）|−1{E0}体（T@m） .ΣE|体（T@m）|− 1必须是一种可接受的方法，特别是，E0和E|体y（T@m）|−1mustnotrefertoolocalarables.262F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255pppppIlwp1（Il）pushcvunshift（El+1[v/s（0）]）pushvxunshift（El+1[x/s（0）]）popx（shift（El+1））[s（0）/x]binopop（shift（El+1））[（s（1）ops（0））/s（1）]gotolJEl'brtruelJ（<$s（0）<$shift（El+1））<$（s（0）<$shift（El'））CheckcastTEl+1τ（s（0））≤TnewobjTunshift（El+1[new（$， T）/s（0），$nT/$]）getfieldT@aEl+1[$（iv（s（0）， T@a））/s（0）]nums（0）nullputfieldT@a（shift2（El+1））[$iv（s（1）， T@a）：=s（0）/$]s（1）/=nullreturntrue图二. wp 1函数的值。 除了brtrue，所有指令都只有一个可能性继承人3.2指令规范VMK指令的所有规则，除了方法调用，都具有以下形式：E1和E2（II）A {El}l：Ilwp1（11）是指令11的局部最弱前提条件。这样的规则表示，Il的前提条件必须隐含Ilw.r.t.的最弱前提条件所有可能的后续指令。wp1的定义如图2所示。在断言中，当前堆栈被称为s，其元素由非负整数表示：元素0是顶部元素，等等。s的解释[El]]：State×Stack→V值为[s（0）]]<$S，（σ，v）<$= v和[s（i +1）]<$S，（σ，v）<$=[[s（i）]]<$S，σ<$。函数shift和unshift分别表示值被推入堆栈和从堆栈中弹出时发生的替换：shift（E）=E[s（i+1）/s（i）for alli∈ N]unshift=shift−1shiftn表示n次连续的移位应用。pushc、pushv和pop的规则类似于霍尔的赋值公理：前提条件是通过将赋值的右边替换为左边的变量从后置条件中获得的。对于push指令，栈顶元素可以被视为左侧变量;对于pop指令，栈顶是右侧表达式。所有其他堆栈引用都通过分别应用unshift和shift函数进行调整。F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255263binop指令弹出两个值，执行二进制操作，并推送结果。因此，移位仅应用一次。无条件jump改变控制流程。因此，其局部最弱的前提条件是跳跃目标的前提条件。一个分支有两个可能的后继，这取决于栈顶的值。它的局部最弱前提条件是从两个潜在后继指令的前提条件中获得的。对于一个检查转换T指令，必须证明它的后继指令的前提条件成立，并且栈顶的类型是T的子类型。由于栈顶元素没有弹出，所以这里没有应用shift对象创建、字段读取和字段更新也类似于经典赋值：putfield更新当前对象存储，getfield更新栈顶元素，newobj更新两者。 getfield和putfield要求接收器对象（堆栈顶部）是非空的。getfield将替换为栈顶指定的实例变量。 因为它弹出并推动一个每个元素，不应用移位。putfield用第二个堆栈元素更新指定实例变量处的当前对象存储。因为它弹出两个值，所以移位被应用两次。方法调用。 对于虚方法T：m的调用，必须证明(1) T：m满足其方法规范，（2）invokevirtual指令的前提条件暗示了方法规范的前提条件，用实际参数代替形式参数，以及(3)方法规范的后置条件意味着在invokevirtual之后的指令的前置条件，结果由栈顶替换。这些要求是invokevirtual规则的前提：汽车旅馆（1）A {P}T：m{Q}空值P[s（1）/this，s（0）/p][shift（w）/Z]Q[s（0）/结果][w/Z]ΔE1+ 1A {El}l：invokevirtualT：m其中Z是向量Z0，.，Zn，并且w是向量w 0，.，wn的局部变量或堆栈元素（不同于s（0））。向量的移位函数是逐点定义的。方法调用不会修改调用方的局部变量和计算堆栈，但弹出参数和推送调用结果除外。为了表达这些框架属性，调用规则允许将方法的前置条件和后置条件中的逻辑变量替换为调用方的局部变量和堆栈元素。但是，s（0）不能用于替换，因为它包含调用的结果，也就是说，它的值不会被调用保留。264F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）2553.3方法规范这一规则的形式是一种对Poetzsch-HelecteranddMu？ller的源程序逻辑的定义。我们在这里简单地总结一下这些规则。详细的解释见[19]。虚方法用于动态绑定方法的建模。 也就是说，T：m的方法规范反映了在调用T：m时可能执行的所有实现的公共属性。如果T是一个类，那么有两个义务来证明虚方法T的规范：m：（1）如果为类型T的对象调用，则相应的实现满足该规范。(2)证明了该规范对T的适当子类型的对象也成立。A <${P<$τ（this）=T}impl（T，m）{Q}A <${P<$τ（this）<$T}T：m{Q}A <${P<$τ（this）≤T}T：m{Q}这个规则的第二个前提和接口类型方法的注释可以通过下面的规则来证明：如果S是T的子类型，则在S对象上调用T：m等价于调用S：m。因此，只要T：m应用于S对象，S：m的所有属性都将延续到T：m：S≤TA <${P<$τ（this）≤S}S：m{Q}A <${P<$τ（this）≤S}T：m{Q}最后，一个方法实现T@m的规范成立，如果它对它的主体成立。为了处理递归，可以假设T@m的指定用于主体的证明。A，{P}T@m{Q}{P}此空}体（T@m）{Q}A {P}T@m{Q}除了公理语义之外，VMK的编程逻辑还包含独立于语言的公理和规则，用于处理假设和建立前后置条件的谓词逻辑与编程逻辑的三元组之间的连接（图3）。这些规则可应用于方法规范。F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255265► {f alse}组件{false} {P}comp{Q}压缩{P}comp{Q}A {P}comp{Q}{P′}comp′{Q′}， A_{P}comp{Q}A {P′}comp′{Q′}{P′}comp′{Q′}， A_{P}comp{Q}A {P}comp{Q}A {P1}组件{Q1} A{P2}组件{Q2}A {P1$>P2}组件{Q1$>Q2}A {P1}组件{Q1} A{P2}组件{Q2}A {P1$>P2}组件{Q1$>Q2}P<$P′A <${P′}comp{Q′}Q′<$QA {P}comp{Q}A {P}comp{Q}A {P<$R}comp{Q<$R}A {P}comp{Q}A {P[t/Z]}comp{Q[t/Z]}A {P[Y /Z]}组件{Q}A {P[Y /Z]}组件{Z：Q}A {P}组件{Q[Y/Z]}A {Z：P}组件{Q[Y/Z]}图三. 独立的规则。 R和t是不引用程序变量的项。Y和Z是不同的逻辑变量。3.4例如为了说明我们的逻辑是如何工作的，我们验证了一个返回其参数的绝对值的方法int abs（int p）为了简单起见，我们假设abs是在一个没有任何子类的Math类中声明的我们证明该方法满足以下规范：{p=P}数学：abs{（P≥0<$result=P）<$（P0<$result=−P）}<逻辑变量P用于从后置条件引用p 必须满足方法规范形式参数不能出现在后置条件中（第二节）。3.1）。为了导出这个三元组，我们首先导出abs的主体的指令规范266F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255为简洁起见）：{p=Pτ（this）=数学表达式this/=null} 0：pushvp{（s（0）0<$P0）<$（s（0）≥0<$P≥0）<$p=P}1：pushc0<<{（s（1）s（0）<$P0）<$（s（1）≥s（0）<$P≥0）<$p=P}2：binop≥<<{（s（0）0<$P0）<$（s（0）≥0 <$P≥0） <$p=P}3：brtrue8<{P0p=P}4：pushc0{P<0s（0）−p= − P}5：pushv p{P0s（1）−s（0）= −P}6：binop−{P0s（0）=−P}7：goto9{P≥0p=P}8：pushv p{（P≥ 0s（0）=P）（P0s（0）= −P）}9：弹出结果{（P≥0 <$result=P）<$（P0<$result=−P）}10：return我们可以很容易地看到，每个指令的前提条件意味着局部最弱的前提条件。例如，指令8：pushv p的前提条件P≥0<$p=P意味着局部最弱的前提条件，（P≥0<$p=P）<$（P0<$p=−P）。<通过主体规则，我们将这些指令规范与abs主体的方法规范结合起来，然后导出Math @ abs的规范（我们将（P ≥ 0）结果= P）结果（P0）结果= − P）由Q表示<{p=Pτ（this）=Maththis/=null}body（Math@abs）{Q}{p=P<$τ（this）=Math}数学@abs{Q}因为Math没有子类，所以我们有τ（this）Mathfalse。因此，我们可以通过推论规则推导出{false}数学：abs{false}{p=Pτ（this）Math}数学：abs{Q}因 为 abs 是 在 Math 类 中 实 现 的 ， 所 以 我 们 有 impl （ Math ， abs ）=Math@abs。因此，我们可以通过结合上述两个三元组来得出证明{p=P<$τ（this）=Math}数学@abs{Q}{p=Pτ（this）Math}数学：abs{Q}{p=P}数学：绝对值{Q}4健全性我们的逻辑在操作语义方面是合理的。在这一节中，我们简要介绍了可靠性证明。完整的证明在我们的技术报告[4]中给出，其中也包含完整性证明。F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255267J我们在方法规范的层面上表达可靠性：如果一个方法规范{P}M{Q}可以被证明，那么它实际上是成立的。在Gordon [10]之后，我们将操作语义和公理语义嵌入到高阶逻辑中（详见[19]）。对于操作语义，sem表示多步关系：sem（C，p，CJ）<$p;C→<$CJ。三元组{P}M{Q}成立的事实被形式化为谓词H（P，M，Q），即定义如下：H（P，p，Q）<$$>（C<$$>{this<$→this0，p<$→p0，$<$→$0}，（），0<$ $>），（CJ<$$>SJ，σJ，lJ<$）：sem（C，p， C）<$IlJ=return<$[[P]]C<$[[Q]]C JH（P，T@m，Q）<$H（this/=null<$P，body（T@m），Q）H（P，T0：m，Q）τ（this）=TP，impl（T，m），Q）可靠性证明通过归纳法在Hoare三元组的导出树的结构上运行 对于具有前因{Pi}Mi{Qi}和后因的规则，[001 pdf1st-31 files]我们证明了（iH（Pi，Mi，Qi））=H（P，M，Q）. 专注在字节码逻辑的特性上，我们将这种翻译简化为两个方法：（1）我们忽略了序列的假设，因为它们对VMK指令的规则并不重要;（2）翻译遗漏了与递归方法的处理相关的归纳论点。这两个方面都包括在[19]中的翻译中由于VMK逻辑中的方法规范规则，特别是语言无关规则，与我们的源逻辑的规则相同，这些规则的证明对于两个逻辑是相同的。我们在此不再重复这些案例。最有趣的情况是主体规则，它将单个指令连接到方法主体（参见第 二 节 ） 。 3.1 ） 。 对 于 这 个 规 则 ， 我 们 必 须 证 明 H （ E0 ， body（T@m），E|体y（T@m）|−1）。但是，更一般的财产，J J JJ J J J<$C<$$>S，σ，l<$， C<$$>S， σ， l<$：sem（C，p， C）<$[[El]]C<$[[ElJ]]C通过对sem（C，p，CJ）的导子长度的归纳证明了这一点. 对于归纳步骤，我们必须考虑推导的每个步骤并证明：J J JJ J J J<$C<$$>S，σ，l<$， C<$$>S， σ， l<$：（p;C→C）<$[[El]]C<$[[ElJ]]C）我们证明这个属性的情况下区分所有可能的指令。这些情况的证明依赖于以下两个替换引理：268F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255ppp引理4.1引理4.2[[E]]S，σ，l[[shift|κ|（E）]] S，（σ，κ），l[[E [s0/s（i0），. ，sn/s（in），y0/x0，. ，ym/xm]]S，σ，l[[E]]<$S [x0<$$> → [[y0]]<$S，σ，l<$，. ，xm<$→ [[ym]]<$S，σ，l<$]，σ [i0<$$> → [[s0]]<$S，σ，l<$，. ，in<$→[[sn]]<$S，σ，l<$]，l<$为了简洁起见，我们只展示了证明的一种情况：pushc。除了invokevirtual之外，所有其他情况都类似，参见[4]。[[El]]S，σnn [[wp1（l：pushcv）]] nS，σnp p⇐⇒[[unshift(El+1[v/s(0)])]]⟨S,σ⟩⇐⇒[[El+1[v/s(0)]]]⟨S,(σ,t)⟩⇐⇒[[El+1]]⟨S,(σ,v)⟩5应用逻辑为了验证一个方法体，必须为它的每个指令找到合适的规范虽然这项任务对于具有复杂控制流程的程序来说可能很麻烦，但在许多实际情况下，可以系统地导出规范在本节中，我们通过一个例子来说明指令规范可以通过最弱前提变换来导出。如果源代码和源程序的证明可用，则指令及其规格也可以通过证明转换获得。5.1最弱前提条件除了方法调用之外，VMK的指令的规则根据局部最弱的前提条件wp1（11）来制定。 对于指令I1的所有可能后继的给定前置条件，wp1（I1）产生I1的最弱前置条件。为了简洁起见，我们在这一小节中忽略了方法调用。一个方法调用的扩展很简单，参见[4，22]。图4示出了计算2p的方法Math@pow2（int p）的主体。我们假设方法后置条件E15是由接口指定给出的。这个例子说明了在有循环的程序中，几条指令的前置条件相互依赖：E14依赖于E3，E 3又依赖于E14。因此，我们不能直接使用局部最弱预处理函数wp1来计算E14。继类-F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255269pL{p=P} 0：pushc1I0. s（0）= 2P-p1：弹出结果I.P−p结果= 2.P−p2：goto11I2Σ结果=2p/= 0 3： pushv pI3. 结果·2 = 2P−（s（0）−1）4：pushc1I.P−（s（1）−s（0））结果·2 = 2.结果·2 = 2.P−s（0）P−p5：binop−I56：pop pI6result·2 = 2 7：pushv resultI7.P− ps（0）·2 = 2 8：pushc2I8. s（1）·s（0）= 2P-p9：binopI.Σs（0）= 2P-p∗10：弹出结果9I10.P−p.P−p结果= 211：pushv pΣ我11结果= 2.P−p（s（0）/= 0）=（p/= 0）Σ12 ：pushc0I12结果= 2.（1）求一个函数的值。P−ps（0））=（p/= 0）Σ13 ：binop/=I13结果= 2s（0）=（p/=0）14 ：brtrue3I14开始.P结果= 2 15：返回I15见图4。方法Math@pow2（int p）的字节码。每个指令规范都可以从后继的规范中构造sical wp-calculi [6]，我们可以使用固定点迭代来解决这种递归依赖关系。此迭代通过控制流程图向后传播方法后置条件Q，指令I1的最弱的前提条件I1在无穷逻辑中定义。 定义局部最弱前提条件wp1（l1）（k），类似于wp1，但指的是在空间中计算的p（k）plJ在所有类型的ILJ中，IL代替ELJ。在我们的技术报告[4]中，我们表明，实际上，预条件是最弱的预条件。（k）|p| − 1 = Q（0）=falseforrl/=|p|−1n（k+1）=wp1（l1）（k）对于l/=|p|−1Ll=WPn∈N0（个）L如果程序员为那些作为循环一部分的分支指令提供了规范，则可以避免固定点迭代。 这个指定通常是循环不变量和计算循环条件的结果存储在s（0）中的属性的结合。在我们的示例中，1ψ4ψ270F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255循环不变量是result=2P−p，循环条件是p/= 0。因此，我们建议，F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）255271ppp我们得到：E14结果=2P−ps（0）=（p/= 0）基于此规范，我们可以通过应用wp 1来计算E14图4中的规格是通过简单的简化从计算的规格中获得的。由于E14没有被构造性地导出，我们必须证明这个规范足够强，以建立后继者E3和E15的规范。也就是说，我们必须显示E14wp1（I14），这很容易：P（结果= 2s（0）=（p/= 0））PP−p（<$s（0）n次移位（结果= 2 ））}5.2源代码证明正如在引言中所解释的，VMK逻辑的设计标准之一是启用证明转换编译器，它将源程序的证明与代码一起转换为VMK。在本小节中，我们通过一个例子来说明这种方法。证明转换编译器基于分别用于语句和表达式的转换函数S和SE这两个函数都产生VMK指令序列及其规范。S从源语句的证明中生成这个序列。SE生成的是源表达式，这是评估的前提。这些函数可以归纳地定义，也就是说，证明树的翻译可以定义为其子树翻译的组合[3]。例如，对于根是while规则的应用的证明树，S的定义如下：{P}l1：转到l 30 1„«不B{eP}S{P}C{eP}l2：S不{eP}S{P}SB C=@{P}while（e）S{<$e<$P}A{P}13：SE（P，e）{shift（P）{s（0）=e}l4：brtruel 2{Pe}翻译功能使用符号标签。{eP}l2和{P}l3分别是通过将S应用于循环体和将SE应用于循环条件而生成的第一指令的前提条件和标签“悬空”前提条件P e是最终方法体中下一条可以很容易地看到，每个指令Il满足Elwp1（Il），也就是说，S生成有效的VMK证明。−p272F. Bannwart，P.Müller/Electronic Notes in Theoretical Computer Science 141（2005）2551E我们说明了证明翻译的源代码版本的方法图4中的Math@pow2（结果缩写为r）：r=1;whiile（p！=0）{p=p-1;r=r*2;}三重{P=p}数学@pow 2.Σr= 2P满足字节码版本以及源代码实现。考虑while循环的源代码证明：T1双头P−p<$r=2p=0···p=p−1;r = r*2;r= 2P-p<$T0r= 2P−p<$while（p/=0）{p=p−1;r = r * 2;}r= 2P−p¯P= 0循环体S（T1）的证明的翻译产生图1中的指令序列的指令3到10。第四章：hnS（T）OP−p诺伊P−p1r= 2p/=03：pushvp，...，s（0）= 210：流行音乐r整个循环的平移S（T0）通过应用上述模式这种转换产生下面的指令序列，其对应于图2中的指令2至14。第四章：S（T0）hnPR= 2o我