Java Card CAP转换器：构造和压缩方法表和常量池的算法证明PVS

COCVPVS1中的Java Card CAP转换器托马斯·热内2托马斯·詹森2维克卡什·科达蒂大卫·皮查迪2伊瑞莎Universit'edeRennes1CNRSCampus de BeaulieuF-35042雷恩摘要Java Card语言是一种精简的Java方言，旨在为智能卡编程。 Java Card指定了自己的类文件格式（Java Card Converted APplet（CAP）格式），该格式针对智能卡有限的空间资源进行了优化。本文讨论了将普通Java类文件转换为CAP格式所必需的算法的认证开发更确切地说，这些算法涉及构造和压缩方法表和常量池。本文的主要贡献是指定和证明这些算法的正确性使用定理证明PVS。1介绍Java Card语言[7]是一种精简的Java方言，旨在编程智能卡。与Java一样，Java Card被编译成字节码，然后在虚拟机上验证和执行[4]，安装在卡本身的芯片上。然而，智能卡的内存和处理器限制需要进一步的阶段，其中字节码从Java的标准类文件格式优化为CAP文件格式[8]。 这种优化的核心是标记化，其中名称（字符串）被标记（整数值）替换。用整数替换字符串减少了代码的大小，并使用标准的面向对象技术vtables更快地查找虚方法。通过将来自同一包的类文件合并到一个CAP文件中的组件化来获得额外的优化。这意味着可以将多个类文件共用的数据1这项工作部分由欧洲IST研发项目2000-26328“验证卡”资助[2] Email：{Thomas.Genet，Thomas.Jensen，David.Pichardie}irisa. fr这是一个初步版本。 最终版本将发表在《理论计算机科学电子笔记》上网址：www.elsevier.nl/locate/entcsGENET JENSEN KODATI和PICHARDIE2共享，并且来自同一CAP文件的类之间的符号引用可以转换为相对于CAP文件的内存在一篇配套文章[3]中，我们描述了一个用于证明Java Card标记化正确性的语义框架。该框架的基本思想是从标记化的具体规范中抽象描述约束，并表明满足这些约束的任何程序变换都是“正确的”。注意，这与证明实际上存在满足这些约束的函数集合无关（在前引书中没有这样做）。）.将“正确性”分解为两个步骤的主要优点这里报告的工作的目的是构造一个可证明正确的程序，将Java Card类文件转换为等效的CAP文件-我们将这样一个程序称为CAP转换器。上述结果大大减少了构造可证正确转换器的证明工作量。对于标记化，只需验证CAP转换器是否遵守在官方语言定义（参见4）中强加的标记化约束，以确保正确性。对于组件化，首先开发一个合并表的抽象理论，然后将该理论实例化到相关的Java Card结构（如常量池），从而促进了证明（见5）。我们在Java Card程序的简化模型上开发了算法和证明，但该方法对完整的Java Card模型仍然有效。本文件的结构如下。我们首先通过描述Java Card类文件和Java CardCAP文件的方法解析之间的差异，直观地解释了标记化Java Card类文件的目的（第2节）。然后我们继续（第3节）描述类文件的PVS形式化和CAP转换器操作的CAP格式第4节介绍了转换器的标记化部分的开发和附带的证明。关于组件化的第5节描述了CAP格式中常量池合并的规范和实现。2Java Card在Java语言中，当在类c的对象上调用方法m时，使用方法查找函数找到字节码：查找：类引用×方法引用→类引用×字节码它实现了虚方法调用的解析。它接受一个类引用c（接收者对象的实际类）、一个方法引用m（签名和声明m的类），并返回该引用GENET JENSEN KODATI和PICHARDIE3最后一次重新定义m的类（在类继承层次结构中可以在c之上），以及字节码本身。在- mat的类文件中，从类c开始，算法递归地在类层次结构中向上搜索方法m的（重新）定义。在决定一个方法是否重新定义另一个方法时，必须考虑Java可见性调制器-见下文。这项研究的主要步骤是(i) 获取实际类的类信息。(ii) 如果m是public：如果m被定义，则找到else查找super如果m是package-visible：如果m是已定义且可见的，则找到else查找superJava类文件中方法查找的过程查找基本功能是标准的：为了找到在dec类中声明的方法m sig的实现，我们递归地搜索m sig的最后一个重写，从当前类开始，在类层次结构中向上移动到dec类。在考虑方法的可见性修改器时，文献中会出现分歧。例如，[1，6]使用“朴素”查找，不考虑可见性修改器。我们对方法查找的定义通过进行测试来dec标志（保护）或dec标志（公共）或act pk = dec pk这个测试确保了被查找的方法的声明在给出候选实现的类中确实是可见的。 这是一个必要条件，使实际的方法能够覆盖一个具有在包dec pk中声明的相同签名的方法。2.1令牌格式Java Card CAP格式基于令牌，即，当引用包、类或方法时，替换名称（字符串）的整数。使用标记而不是名称减少了代码大小，并允许使用标记作为方法表的索引进行更直接的方法查找，如下所述查找功能查找：类引用×方法引用→类引用×字节码对于CAP格式（如图2所示），它与类文件格式查找函数的不同之处在于，它使用方法表来加速方法定义的搜索。方法表将方法标记与实现该方法的代码的地址相关联，因此查找函数可以直接跳转到该方法，而不是在类层次结构中搜索它（参见图3）。使用标记作为方法表的索引对方法标记化的方式施加了特别重要的是，GENET JENSEN KODATI和PICHARDIE4lookup_name（act_class，（m_sig，dec_class））=让dec_pk=pack_name（dec_class）act_pk=pack_name （ act_class ） （ _ ，_，meth_dec，_，_）= env_name（dec_pk）（dec_class）（_，super，_，meth_act，_，_）= env_name（act_pk）（act_class）（dec_flags，_）= meth_dec（m_sig）在如果meth_act（m_sig）= undefined，则lookup_name（super，（m_sig，dec_class））else ifdec_flags（protected）或dec_flags（public）或act_pk = dec_pk然后let（_，_，code）=meth_act（m_sig）in（act_class，code）else lookup_name（super，（m_sig，dec_class））图1.一、类文件格式的查找函数重新定义另一个方法的方法会收到与它重新定义的方法相同的令牌。在图3中，类B中的方法bar接收与类A中的方法bar相同的标记（2）。因此，一个方法调用X.bar（），其中X的类型为A我们回到第4节中对约束的形式描述Java Card CAP格式规定为一个类生成两个方法表：一个用于类的包外可见的方法（我们称之为公共方法），另一个用于只在包内可见的方法（我们称之为包方法）。方法表可以是部分的，因为并非所有方法都是由一个类需要在方法表中有一个条目。Java Card CAP格式为每个方法表包含一个基;令牌小于此基的方法不包含在表中。因此，这些方法不能通过在方法表中查找来找到，而必须通过搜索类层次结构来找到，就像在类文件格式中所做的那样（参见图2）。此功能的动机是节省空间。从表中省略某些方法意味着方法表占用更少的空间，但代价是减慢了方法查找的速度。3类文件和CAP格式在本节中，我们将介绍类文件格式和CAP格式的PVS规范。它们中的每一个都被构建为PVS抽象数据类型，定义为它的构造函数集、关联的识别器谓词和访问器。PVS模型是Java Card类和CAP文件的强理想化版本。GENET JENSEN KODATI和PICHARDIE5lookup_tok（act_class_ref，（method_tok，dec_class_ref））=let方法=方法数组（act_class_ref）let（_，super，（public_base，_，public_table），（package_base，_，package_table），_）=class_info（act_class_ref）在ifmethod_tok div 128 = 0 then /* public */ifmethod_tok >= public_base thenletmethod_offset = public_table[method_tok-public_base] in如果method_offset> 0xFFFF，则(act_class_ref，methods[method_offset].Bytecode）else/* 在超类中查找 */lookup_tok（super，（method_tok，dec_class_ref））else /* 在超类中查找 */lookup_tok（super，（method_tok，dec_class_ref））else /* package */ifmethod_tok >= package_base and same_package（dec_class_ref，act_class_ref）然后let method_offset= package_table[method_tokmod 128-package_base]in（act_class_ref，methods[method_offset].Bytecode）else /* 在超类中查找 */lookup_tok（super，（method_tok，dec_class_ref））图二. CAP文件格式的查找classA {foo（）{code1> };{code2> };}classBextends A{bar（）{code3> };{code4> };}令牌化A.foo1A.bar2B.bar2B.baz3图三.方法的标记化方法表1&code12&code21&code12&代码33&代码4我们从所有与我们的算法考虑无关的细节中抽象出来。下面的证明扩展到一个更精确的模型，但细节会掩盖发展和介绍。GENET JENSEN KODATI和PICHARDIE63.1类文件格式类文件格式是Java（Card）类文件层次结构的理想化版本在最顶层，类层次结构表示为森林（而不是树），如下所示：ClassHier：DATATYPEBEGIN空：空的？nodeHier（ class： ClassFile，儿子：ClassHier，brothers： ClassHier）： nodeHier？END类这种更通用的表示具有这样的优点，即它同样可以很好地建模完整Java Card程序的类树和构成单个Java Card包的类森林此外，从证明论的角度来看，这种表示具有良好的性质。特别是，使用的证据，通过归纳在一个ClassHier结构ch，产生一些归纳假设的儿子和兄弟层次的ch是相同类型的ch。当使用一个层次结构ch有一个子列表的结构时，情况就不是这样了：相关的归纳假设是在一个类型列表[ClassHier]的对象上。在这种情况下，归纳原理更复杂，因为它是ClassHier和list[ClassHier]上的互感。类层次结构是一个森林，可以是空的，也可以是nodeHier（c，s，b）的形式，其中c是一个类，s是其子类的森林，b是兄弟类的森林。例如，一个类c1有两个子类c2和c3，可以用一个项nodeHier（c1，nodeHier（c2，empty，nodeHier（c3，empty，empty）），empty）来表示，其中c1有一个子类c2，子类c2有一个兄弟类c3。 在上面的数据类型中，class、sons和brothers是访问器，为空？，nodeHier？是识别器。ClassFile类型本身是一个PVS记录结构，有四个字段：ClassFile：TYPE=[#super：Maybe[ClassRef name]，methods：Methods name，name：ClassRef name，cp：CP名称#]每个类文件包含一个对超类super的引用（对于最顶层的类来说可能是空的），在类方法中定义的方法列表，对类本身名称和常量池cp的引用。常量池（由常量数组表示）将在第5节中更精确地定义GENET JENSEN KODATI和PICHARDIE73.2CAP格式CAP格式是将标记替换为（方法、类和包）名称并将常量池重新分组为整个包的一个常量池组件的结果。因此，CAP文件格式的数据类型与Class File数据类型非常相似，只是标记替换了所有地方的名称，并且整个包有一个唯一的常量池。因此，Package是与标记化常量池相关联的标记化层次结构：软件包：类型=[#包：ClassHier tok，cp：CP tok#]ClassHier tok：DATATYPEBEGIN空的：空的tok？nodeHier（class：ClassFiletok，sons：ClassHier tok，brothers：ClassHier tok）：nodeHier tok？ENDClassHier tokClassFile tok：TYPE=[#super：Maybe[ClassRef tok]，methods：Methods tok，name：ClassRef tok#]4Java Card类文件的令牌化在本节中，我们首先介绍一种算法，根据CAP格式的定义，为类层次结构中的每个类构建相应的方法表。在第4.2节中，我们证明了一些定理，这些定理共同证明了标记化算法的有效性。算法用PVS规范语言表示-参见[5]的描述。4.1程序我们在这里提出的算法计算令牌表的类层次结构。标记表将方法映射到其对应的标记，并且是用于构建方法表的关键数据结构。 该算法由几个函数组成，这些函数遍历类层次结构，对于每个类，首先将类中定义的方法标记化，然后构建方法表 为了上课遍历类层次结构函 数 tokHier 将 层 次 结 构 h （ ClassHier 类 型 ） 转 换 为 类 似 层 次 结 构（ClassHier类型wtt），其中类的类型被丰富GENET JENSEN KODATI和PICHARDIE8一个与类中定义的方法列表相对应的标记表以及继承的方法。注意，对于给定的类层次结构h，由于h的方法的标记编号取决于h上面定义的方法的标记编号，因此tokHier需要h的超类的标记表。这个令牌表分为两部分提供给tokHier：公共的mt super pub和包的mt super pack。 如果h没有超类，那么这两个表是空的。tokHier函数使用tokClass函数在h的顶部构造类的标记表，并递归地转换h的子和兄弟层次结构。请注意，PVSMEASURE关键字引入了用于证明递归的良好基础的度量，从而终止函数。在tokHier的特定情况下，由于层级h是递减的（w.r.t. 递归（subterm排序）。tokHier（h：ClassHier，mt super pub，mt super pack：TokenTable）：RECURSIVEClassHier wtt=（案件h）空的：empty，nodeHier（c，h sub，h rest）：LET（mt cPub，mt cPack）=tokClass（c，mt super pub，mt superpack），mt sub=tokHier（h sub，mt cPub，mtcPack），mt rest=tokHier（h rest，mt super pub，mt super pack）在nodeHier（（#super：=c苏布山、雷斯特山）ENDCASES）测量H<<类的标记化函数tokClass计算token的public和package表，一个类c，知道超类token的public和package表。首先，c的方法列表被拆分成一个公共列表和一个私有列表（函数拆分方法）。然后，调用tokClassList来计算每个列表的token表。tokClass （ c ： ClassFile ， mt super pub ， mt super pack ：TokenTable）：[TokenTable，TokenTable]=LET（lPub，lPack）=拆分方法（c（tokClassList（c对于一个给定的类名c，使用方法列表listMet和超类mt super的令牌表，函数tokClassList构造令牌表GENET JENSEN KODATI和PICHARDIE9对应于listMet和继承的方法。integer fieldnext在递归调用期间用于计算mtsuper中定义的每个方法，以便找到可用于对listMet中的方法进行标记化的第一个标记的数量。如果方法s与mt super中的tokent相关联，并且如果s出现在listMet中，则searchMethod函数确保s将由类c中的相同tokent编号。tokClassList（c：ClassName，next：MethodToken，listMet：Methodsname，mt super：TokenTable）：RECURSIVETokenTable=（例超级山OFnull ：listMetToTokenTable （ c ，listMet ，next）， cons（s， rest）：LET（new s，new listMet）=searchMethod（c，s，listMet）INcons（new s，tokClassList（c，next+ 1，new listMet，rest））ENDCASES）测量超级山<<4.2验证标记化为了证明标记化算法规范的正确性，正如在引言中指出的那样，只要证明该算法满足Sun的规范中描述的约束就足够了。这个证明包括了100多个用PVS证明的引理，并分为四个部分：重新定义的方法的标记化，新方法的标记化，继承方法的标记化和标记分布。在这里，我们给出了证明的每一部分的解释。4.2.1重新定义的方法其中一个约束指出，当一个类定义了一个已经存在于类的超类中的方法时作为一个例子，下面是PVS语法中公共方法的特殊情况的引理方法重新定义1：引理（h：ClassHier，c1，c2：ClassFile wtt，mt super pub，mt super pack：TokenTable，m：[Sig，MethodInfo name]）：LETh2=tokHier（h，mt super pub，mt super pack）INValidHierarchy（h）子类（c1，c2，h2）成员（m，c1member（m，c2⊃（n（s1，s2：TokenTableStruct）：member（s1，c1s% 1∀GENET JENSEN KODATI和PICHARDIE10member（s2，c2s1引理方法重新定义1说，如果c1是层次结构h2（类层次结构h的标记化版本）中c2的子类，m是在两个类中定义的方法，那么m将出现在两个对应的表中，相同的标记，但具有相对类的不同名称。 层级h被认为是所谓的有效层级，意味着例如在层次结构中没有类出现两次。这个引理的证明是基于对层次结构h的归纳。• 如果h是空的，这与c1是c2的子类的事实相矛盾，所以• 如果h是类c的一个节点，一个子层次hsub和一个兄弟层次hrest，有三种情况要研究(i)c2等于c，c1是一类hsub(ii)c1是层次结构hsub中c2(iii)c1是层次结构hrest中c2关于包表的证明（重新定义的引理方法2）是类似的。4.2.2一种新方法当一个类定义了一个新的公共类时，package）方法（即一个没有出现在超类中的方法），它必须有一个比超类public中使用的所有token都要大的token。包）表。对于新的公共方法，此条件以以下方式表示新方法1：引理（h：ClassHier，c1，c2：ClassFile wtt，mt super pub，mt super pack：TokenTable，m1，m2：[Sig，MethodInfo name]）：设h2=tokHier（h，mt super pub，mt super pack），ValidHierarchy（h）n成员（c1，h2）n成员（m1，c1m1会员（m1（C2：ClassFile wtt）：子类（c1，c2，h2）成员（m1子类（c1，c2，h2）member（m2，c2⊃（（s1，s2：TokenTableStruct）：[3]更确切地说，是c2的限制，我们省略了表。∀GENET JENSEN KODATI和PICHARDIE11member（s1，c1s1这个引理陈述了一个属性，其中c1是层次结构h2中c2的子类，层次结构h2是类层次结构h的标记化版本。如果c1定义了一个新的方法m1（since<$member（m1'1，mt super pub）），如果c 2定义了一个方法m 2，那么用于m 1的token（s 2 'token）大于用于m 2的token（s 2'token）。证明需要在层次上进行双重归纳。对于包表，证明是类似的。4.2.3继承方法在类中定义的每个方法都必须有一个标记，但不仅仅是这些方法。也有一个继承方法的标记。因此，有必要证明在类c2中定义的公共方法将出现在具有相同令牌的所有子类的公共令牌表中，直到子类重新定义该方法。4.2.4令牌分发一些引理也是必要的，以证明该规范的最终要求，即。公共表中的所有标记都在区间[0，length（table）-1]中，并且该区间中的每个值都对应于表中的标记5合并常数池在Java字节码格式中，整数、实数、字符串、类和方法名称等常量都存储在一个称为常量池的数组中。每个类都有一个常量池。在类的方法的字节码中，常量的每次出现都被常量池中相应的索引替换。本节介绍Java Card包的组件化Java Card定义了一个类文件包必须如何被分割成多个组件（方法、类、导出、常量池等），这些组件一起表示这个包。我们将不涉及组件化的所有这些方面，而是关注如何构建常量池组件。更准确地说，我们将展示如何定义和证明一个函数是正确的，这个函数被赋予一个类层次结构，并产生两个结果：一个全局包常量池和一个O函数集函数f。全局常量池是通过合并层次结构中包含的类的所有常量池而产生的对于层次结构中的每个类，o_n_set函数给出了在全局常量池中执行的跳转，以查找该类的常量池的内容。特别是，o_nset函数将用于对每个GENET JENSEN KODATI和PICHARDIE12--−Java Card包的名称为n的类：在名称为n的类的字节码中，每次出现索引i都将被i+f（n）替换。因此，在组件化函数上要证明的主要性质是，对于在层次结构中的名称为n的每个类c，c的全局常量池的第i个单元的内容等于全局包常量池的第（i+f（n））个单元的内容函数及其相关证明可以分为两个更简单的问题：• 将两个常量池合并在一起，• 在类层次结构上应用这个简单的合并函数，将所有常量池收集到一个全局常量池中，并使用一个正确的o_set函数。在5.1节中，我们定义了一个特殊的理论来处理基本的数组复制和合并问题。在第5.2节中，我们展示了如何使用这个简单的理论来实现组件化函数及其在类层次结构上的证明。5.1数组合并理论为了在PVS中表示常量池，我们选择了一个相对较低的表示级别，以便精确地建模数组及其边界。所选的表示使用PVS依赖类型：cpool：TYPE=[# size： nat， tab：[ below[ size]→ Content]#]因此，常量池是一种记录类型，其中size字段表示数组的大小，tab字段包含数组本身。这个数组是一个全函数，映射每个0的索引... size-1为Content类型的元素。根据包含此常量池的格式，内容类型将由不同类型实例化：类文件格式的方法名称和CAP格式的方法标记。注意，常量池的大小可以是0，正如Java规范[8]中所提到的。然后，定义数组访问和数组修改是简单的：read（t： cpool，k： below[ size（t）]）： Content= tab（t）（k）put（t：cpool，k：below [size（t）]，e：Content）：（t1：cpool|size（t）=size（t1））=（#size：=size（t），tab：=tab（t）WITH[（k）：=e]#）在这两个定义中，请注意我们使用了子类型。实际上，read的类型定义说的是，一个人只能在常量池t中读取类型低于[size（t）]的位置，即。 间隔0... 1号是自然的一种亚型。同样，对常量池t调用put函数将返回子类型为{t1：cpool}的常量池|size（t）= size（t1）}，即类型和tPVS有很强的处理在判定过程大量使用子类型信息并导致更大自动化的证明中使用子类型。 然而，GENET JENSEN KODATI和PICHARDIE13必须小心使用例如，递归函数arraycopy，其类型为：arraycopy（t1：cpool，from pos：below[size（t1）]，到pos：{i| frompos≤ii0验证Hier（ch）验证（（i：below（size（cp）：read（cp，i）=read（comp cp，get（get asleep（ctok，o））+i））然而，这个定理的类型提出了两个非平凡的证明义务（TCC），揭示了两个必须首先证明的隐含假设，作为引理。 第一个引理指出，通过在关联列表中查找类cf的名称，我们将获得至少一个跳转值，即o_set函数对于层次结构的类名是全的。第二个引理指出，对于每一个类文件cf，jump+i都在全局成分化常数池comp cp的范围内。即使细节是相当不同的，这两个引理和正确性cp分量的整体证明草图是相似的。 我们对层次结构ch的结构进行归纳。空层次结构的基本情况很容易被丢弃，因为它与cf已知在层次结构ch中的事实相矛盾。然后，对于一般情况下，我们实现了对定义的案例证明，GENET JENSEN KODATI和PICHARDIE17成员（cf，ch）：• 如果cf在层次结构的顶部，我们需要证明结果是正确构造的，并且对子和兄弟递归调用的结果的最终聚集不会修改其有效性。• 如果CF在当前节点的子节点或兄弟节点中，则我们需要使用归纳假设来获得部分结果的属性，然后，如在先前的情况下，检查该属性是否通过收集剩余结果而被保留。6结论我们已经详细说明了PVS中CAP转换器的核心算法。这些算法处理JavaCard类文件的标记化和组件化。标记化算法被证明是正确的，它满足了CAP格式的Java Card定义中详细描述的约束。正如在以前的工作[3]中所示，这足以证明转换的正确性。在合并常数池的特殊情况下，证明了离散化是正确的。这项工作是在Java Card的环境中进行的，但底层的优化原则适用于任何使用方法表来实现动态方法调度的面向对象语言。此外，在该方法中没有强制使用PVS定理证明器。选择PVS主要是因为它方便的规范语言和它的证明自动化程度，这显然是有益的。这些证明是基于程序模型的，这些模型抽象出了Java Card格式的许多特性，但我们相信这些格式是解决核心算法问题的正确格式。没有根本的原因为什么结果不应该延续到一个更详细的然而，转换器的规格和验证是一项长期而艰巨的任务。在许多验证工作中，证明的复杂性主要是由于要检查的程序的大小。在我们的例子中，程序相当小，但复杂性在其他地方，而且是双重的。首先，CAP格式相当复杂，需要投入一定的时间来研究Sun的操作规范，以便将Java和JavaCard格式抽象为相关的PVS模型。接下来，为了将程序的低层动作包含到验证中，PVS模型的某些方面也是低层的，需要一些低层引理和验证。在这两个方面，PVS类型检查条件对于检测指定的弱点非常有用例如，零大小的常量池或隐式地做出的假设，例如，类层次结构的格式良好。转换器本身的具体说明只有1873行PVS;然而，整个证明由100多个引理和6500行策略组成。虽然许多作品都涉及验证编译器优化GENET JENSEN KODATI和PICHARDIE18对于不同的语言和不同程度的自动化，我们知道只有一件工作直接解决了这里研究的优化类型。Denney [2]展示了如何使用Coq的程序提取机制开发Java Card转换器。更确切地说，从一个建设性的证明，对于每个Java卡程序存在一个等价的程序在转换格式，它是如何提取这样的转换器。与我们的工作一样，强加了一些限制：只考虑包可见的方法，并且没有详细说明常量池的合并。然而，这是有史以来使用程序提取构建的最重要的程序之一。正如在[2]中所指出的，程序提取远不是一种“按钮”技术，需要开发人员相当多的Coq专业知识。我们相信，我们的“编程然后证明”方法更容易获得，尽管它仍然需要一定程度的专业知识（在这种情况下是PVS）。程序提取是否可以通过将其与高度的证明自动化相结合而变得同样可访问是开放的。鸣谢：感谢Yoann Padioleau对本文草稿的详细评论。引用[1] P. Bertelsen. Java字节码的语义。技术报告，丹麦技术大学信息技术系，1997年3月[2] E.丹尼Java Card令牌化算法的合成。在proc 第16届国际自动化软件工程会议（ASE 2001），第43-50页。IEEE Press，2001.[3] E. Denney和T.詹森。通过逻辑关系查找Java Card方法的正确性理论计算机科学，283：305[4] T. Lindholm和F.大喊大叫。Java虚拟机规范艾迪生-韦斯利，1997年.[5] S. Owre，J.M. Rushby，和N.史恩卡PVS：原型验证系统。在Proc. of 11 th Int.Conf. on Automated Deduction（ CADE），LNAI的卷 607，页748-752 中。Sp