源码翻译的浅层表示与其深层表示的等效性证明

理论计算机科学电子笔记164（2006）61-79www.elsevier.com/locate/entcs结合深嵌入和浅嵌入Joni Helin琼尼·赫林1，2芬兰坦佩雷理工大学软件系统研究所摘要本文提出了一种在源语言具有形式语义的情况下验证翻译器正确性的方法。 而不是验证翻译器的实现，一种新的语言机械化组合的设计，以减少总的复杂性。深度嵌入被定义为特定含义的基线。对于每个规范，构造并进行等价性证明，以确保翻译后的浅层表示在语义上等价于深层表示。 结构等价性证明是系统的，可以从具体结构中机械地推导出来。的两个嵌入的使用还通过使得能够以更简单的方式定义嵌入而有利地改进了嵌入。保留字：形式规范，翻译器正确性，浅嵌入，深嵌入，OCSID1引言无论我们是在设计一门编程语言还是一门形式语言，语言实现都是我们工作的重要组成部分。如果要获得工具正确性的最终信心然而，关于编程语言构造的推理是困难的，并且翻译器往往是相当复杂的代码段。因此，我们更倾向于另一种方法，其中通过较小的总当量实现相同的结果。在本文中，我们提出了一种替代方法，工具的正确性时，源和目标语言有正式的语义。而不是验证translator实现，我们利用两个同声翻译。该方法的目标是通过采取更小的步骤来减少所涉及的总的电子邮件数量和复杂性。[1]Joni Helin由芬兰科学院资助201064。2 电子邮件：joni. tut.fi传真：+358 3 3115 29131571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.00562J. 贺林/理论计算机科学电子笔记164（2006）61这种方法需要建立一个语义尺度，以便将原文的浅层翻译结果与之进行比较。为此，我们使用深度嵌入，这本质上是一种形式化的语言定义。深度嵌入还可以增加我们对语言定义的意义的信心;我们可以陈述它应该展示的属性，并使用定理证明器来验证它们。使用两种翻译表明，我们会产生一些额外的工作，但我们认为，在正确的情况下，所需的e-的数量级较小。降低复杂性的关键因素在于等价性证明的结构;它们可以从规范中系统地推导出来。对于本文中提出的方法的适用性，嵌入式语言的确切细节并不重要。必要的是要有一个精确的意义与程序或规格写的语言。我们框架的讨论，我们的方法与机械化的实验规范语言Ocsid的主机逻辑提供的定理证明PVS。本文的其余部分组织如下。第2节讨论了编程逻辑的机械化方法。第3节介绍了规范化语言Ocsid，第4节中使用它来演示所提倡的技术的具体应用。第5节讨论了与产生和进行等价性证明有关的问题第6节介绍了相关的方法，第7节总结了本文。2嵌入编程逻辑由于我们正在开发一种正式的规范语言，我们自然必须为用户提供正式推理其规范属性的能力。而不是建立一个专用的证明系统，推理支持通常是通过在高阶逻辑中机械化语言来提供的，即将语言嵌入一般定理证明器逻辑[5]。有两种主要的嵌入方案，浅和深。为了本文的目的，我们在这里只对它们的区别作一个简要的解释。 读者可参考已发表的更详尽的讨论。在[2]中。在浅嵌入中，程序或规范的含义通过转换为宿主逻辑中的语义等价表示来保留。相比之下，深度嵌入在宿主逻辑中显式地表示语言的语法，并提供解释其含义的语义功能。这给了我们机会去思考语言本身，而不仅仅是具体的程序。很容易看出，语言嵌入需要的间接性越少，嵌入式程序的推理就越简单。深度嵌入对于定理证明器的自动决策过程也是一个挑战，这是为手写规范而设计的。由于这些原因，浅嵌入在实际验证中往往是可取的。从语言设计者的角度来看，J. 贺林/理论计算机科学电子笔记164（2006）6163语言的合理性。虽然浅嵌入很容易使用，但它并不便于对语言属性或程序类进行全面推理。这是因为语法构造并不作为第一个类值保留，而只是隐含在嵌入式程序的结构中。语言定义和浅层翻译之间的联系因此，对实现正确性的信心必然缺乏。由于深度嵌入不受这些限制，有时可能会牺牲浅嵌入的好处。从上面的讨论中可以明显看出，两种嵌入方法都有各自的优点和缺点。而不是承诺一个或另一个，本文继续展示如何将它们有效地结合起来使用3 Ocsid概述为了将讨论固定到具体的设置中，我们使用实验规范语言Ocsid。为了更好地说明本文所倡导的方法，我们只对基本思想进行了简要介绍，并简化了技术细节。感兴趣的读者可以参考[6]，以更完整地讨论完整的功能和方法学意义。Ocsid是一种基于视图的分布式协作分解的规范语言。它是一种面向状态的形式主义，其语义基于动作的时态逻辑（TLA）[7]。Ocsid采用了一个基于对象的框架，其中使用类、对象和数据成员对数据进行建模。一个系统由任意数量的对象组成。对数据成员的操作使用联合操作[3]表示，联合操作对协作中参与对象的同步进行建模。一个联合动作由一个声明正式参与者的角色列表、一个守卫和一个主体组成。守卫确定联合动作对于参与对象的特定组合的执行资格。联合行动的主体指定了对参与者的数据成员的集体影响，但忽略了实现这些影响所必需的通信协议。执行是不确定的，因为在执行的每个状态中，启用的操作之一变为选定。并发是通过交错来建模的，即独立的动作可以以任何顺序发生。Ocsid的视图机制允许规范的模块化以匹配行为关注点。每个视图仅指定验证特定视图不变量所需的结构和行为方面，并且定义视图的组成以保留视图的不变量。为了使其可行，视图已关闭。在封闭世界建模中，如果一个specification包含一个状态变量，它也包含所有分配给它的操作。这种突变的完整性允许通过孤立地考虑视图来推理时间安全属性。下面给出了一个人为的示例视图。它指出，当两个参与对象的变量x的值相等时，第一个对象的值为64J. 贺林/理论计算机科学电子笔记164（2006）61递增。一个系统满足这个观点，如果在执行的每一步，它要么卡顿（保持变量不变），要么两个合格的C类对象同步更新变量x作为动作A指定。简单视图为C类变量C.x：integer;c1.x = c2.x时c1，c2：C的操作Ac1.x：= c1.x + 1;end端4嵌入Ocsid本节演示了使用两个错误的嵌入来实现Ocsid语言的机械化作为主机逻辑，我们采用PVS [9]的逻辑，由于其高阶性质，它是合适的。PVS的另一个优点是它的逻辑包含一个可执行子集[10]，可以用作函数式编程语言。提供了一种用于评估可执行PVS功能的地面评估器。这允许计算语法转换的结果。图1示出了机械化布置的基本元件如何相互关联的描述。4.1公共语义库下面给出的PVS类型声明定义了Ocsid的时态元素的语义基础。这些是浅嵌入和深嵌入之间共享的。这一点很重要，因为它有助于以后连接两个嵌入。状态：类型+BEHAVIOR： TYPE= sequence[STATE]STEP： TYPE= [STATE，STATE]ACTION： TYPE= [STEP -> bool]质量标准：类型= pred[行为]类[ref_type：TYPE+]：DATATYPEBEGINobject（reference：ref_type）：object？ENDclass这里STATE是一个未解释的类型，它定义了所有可能规范中所有可能状态的集合动作是步骤（状态对）上的谓词，即它决定动作是否在起始状态下启用，并且是参与组合可能的指定结果状态。同样，一个规范在语义上是一个谓词，J. 贺林/理论计算机科学电子笔记164（2006）6165浅层编译器深度编译器验证生成器规范深层表征浅表示是/无结论Fig. 1.机械化要素行为。在这一点上，我们不提供我们的数据设施的定义，即变量和值。当我们进入动作的细节时，它们是必需的，但是由于它们的表示依赖于所使用的嵌入，它们不能被包括在公共基础中。4.2Ocsid的深度嵌入下面显示的是使用PVS代数数据类型的Ocsid视图的抽象语法。这种描述与BNF用于相同目的的传统用法非常相似。每个数据类型定义都列举了构造函数来生成值（句子），列出了它们的参数，并提供了识别器谓词来确定应用的构造函数。参数隐式地定义了构造函数参数的访问器函数。句法Ocsid表达式的一个子集显示时，它们的语义定义。深度嵌入的使用允许我们公式化和证明句法操作的性质。例如，在Ocsid中证明复合只需要在所有可能的视图对上进行语法归纳然而，省略了特定于八进制的语法转换，因为它们与嵌入方法PVS等效性证明66J. 贺林/理论计算机科学电子笔记164（2006）61本文提倡。type_syntax：类型=名称idclass_syntax：class（name： nameid）：class？END类语法变量语法：DATATYPE BEGIN变量（名称：名称ID，类：class_syntax，类型：type_syntax）：变量？END变量语法formal_parameter_syntax：数据类型开始formal_param（name：nameid，type：type_syntax）：formal_param？formal_role（name：nameid，class：class_syntax）：formal_role？端形式参数语法assignment_syntax：数据类型开始assignment（obj：（formal_role？），field：variable_syntax，rhs：expr_syntax）：赋值？END赋值语法action_syntax：数据类型开始action（name：nameid，roles：list[formal_parameter_syntax]，guard：list[expr_syntax]，body： list[assignment_syntax]）：action？END操作语法view_syntax：DATATYPEBEGIN视图（名称：名称ID，classes：list[class_syntax]，variables：list[variable_syntax]，actions：list[action_syntax]）：view？END视图语法在这个演示中，我们定义了一个基本的嵌入，其中故意忽略了键入信息。这是合理的，因为我们有两个嵌入，其中深的一个主要是作为规范行为的尺度。因此，经典的静态分析，如类型正确性，可以相当一致。J. 贺林/理论计算机科学电子笔记164（2006）6167假设由PVS类型系统在浅嵌入中处理。这大大降低了深度嵌入的大小和复杂性。这种简化带来的一个约束是，不再可能定义依赖于类型信息的语法转换，但这里不需要这些。深度嵌入的语义域如下所示。首先，未解释的类型OBJECTIVE声明所有对象的集合。代数数据类型VALUE为我们简化的类型化方案中的值提供了构造器、访问器和重命名器VARIABLE被定义为从对象和状态到值的映射。未解释的映射函数表示从类、类型和变量的句法表示到它们的语义对应物的连接环境是一个记录，它将句法域中的动作角色和其他参数绑定到语义域。对象：类型值：数据类型开始error_value：error_value？integer_value（intval：integer）：integer_value？boolean_value（boolval：boolean）：boolean_value？reference_value（refval：object）：reference_value？lambda_value（lambda_value：[value -> value]）：lambda_value？结束值变量：类型= [对象，状态->值]type_map：[nameid -> pred[VALUE]]，class_map：[class_syntax ->pred[OBSTAL]]，var_map：[variable_syntax->VARIABLE]，环境：TYPE= [# objmap：[（formal_role？）->对象]，parmap：[（formal_param？）->数值]#]接下来给出更有趣的语义函数视图语义定义如下。它指出，对于满足给定视图规范的行为，对于行为中的所有步骤，必须有一个适用的操作，或者步骤必须是断断续续的（视图变量的值不变）。sem（v：view_syntax）：规范= LAMBDA（b：行为）：（FORALL（n：nat）：（EXISTS（a：action_syntax）：member（a，actions（v）） ANDsem（a，classes（v），variables（v））（b（n），b（n+ 1）ORsem（stuttering_action，classes（v），variables（v））(b(n)，b（n+ 1）68J. 贺林/理论计算机科学电子笔记164（2006）61动作语义详细介绍了保护和主体。 第一个函数是一个简单的转发到执行实际处理的递归函数。首先，else分支将合适的存在量化的参与者对象绑定到角色。第一部分确保所有的守护合取在第一（未启动）状态下得到满足。其次，它迭代视图的所有类，并通过普遍量化它们的对象，确保它们在第二（启动）状态下的所有场的值对应于在主体中分配给它们的值sem（a：action_syntax，class：list[class_syntax]，vars：list[variable_syntax]）：ACTION =LAMBDA（now，next：STATE）：sem（a，now，next，empty_env，roles（a），classes，vars）sem（a：action_syntax，unprimed，primed：STATE，env：environment，roles：list[（formal_role？）]，classes：list[class_syntax]，vars：list[variable_syntax]）：RECURSIVEbool=如果为空？（roles）THEN every（（LAMBDA（g：expr_syntax））：布尔值（sem（g，env，unprimed），保护（a））和every（（LAMBDA（class：class_syntax））：（FORALL（obj：（class_map（class）：（every（（LAMBDA（field： variable_syntax）：（var_map（field）（obj，primed）= primed_value（body（a），unprimed，env）（obj，field），filter（（LAMBDA（f：variable_syntax）：class（f）=class），vars），类）其他EXISTS（obj：（class_map（class（car（roles）：sem（a，未启动，启动，env WITHWITH[（car（roles））：= obj]]，cdr（roles），classes，vars）ENDIFMEASURE长度（角色）函数primed value负责计算动作体中as-value的右侧。它构造了一个从对象和字段到它们的初始值的映射，如果没有为组合指定显式赋值，则默认为口吃J. 贺林/理论计算机科学电子笔记164（2006）6169primed_value（assignments：list[assignment_syntax]，70J. 贺林/理论计算机科学电子笔记164（2006）61unprimed：STATE，env：environment）：RECURSIVE[OBSTATE，variable_syntax ->VALUE]=如果为空？（任务）THEN LAMBDA（obj： OBJECTIVE，field：variable_syntax）：var_map（field）（obj，unprimed）其他案例汽车（任务）OF赋值（role，f，rhs）：primed_value（cdr（assignments），unprimed，env）函数名：函数名：= sem（rhs，env，unprimed）]最终案例ENDIF测量长度（赋值）下面给出了所选择的句法表达和相应的语义功能。它们是句法域和语义域之间相当直接的映射。包括通用量化和lambda形式来演示对象和类型谓词的使用以及环境操作。expr_syntax：数据类型开始intconst（v： int）：intconst？var_ref（obj：（formal_role？），field：variable_syntax）：var_ref？plus（e1，e2：expr_syntax）：plus？equal（e1，e2： expr_syntax）：等于？forall_q（q_var：（formal_role？），e： expr_syntax）：forall_q？lambda（param：（formal_param？），body：expr_syntax）：lambda？application（comp，arg：expr_syntax）：application？END expr_语法sem（e：expr_syntax，env：environment，s：STATE）：递归值=案例e的intconst（i）：integer_value（i），var_ref（role，f）：var_map（f）（objmap（env）（role），s），plus（e1，e2）：integer_value（intval（sem（e1，env，s））+ intval（sem（e2，env，s）），equal（e1，e2）：boolean_value（sem（e1，env，s））= sem（e2，env，s）），forall_q（qvar，e）：boolean_value（FORALL（o：（class_map（class（qvar）：boolval（sem（e，env WITHJ. 贺林/理论计算机科学电子笔记164（2006）6171与[（qvar）：= o]]，s）），lambda（pr，body）：lambda_value（LAMBDA（v： VALUE）：IF type_map（type（pr））（v）THENsem（body，env WITH72J. 贺林/理论计算机科学电子笔记164（2006）61WITH[（pr）：= v]]，s）ELSE error_value ENDIF），应用程序（comp，arg）：sem（comp，env，s）（sem（arg，env，s））测量方法e<<4.3浅埋浅嵌入由Ocsid编译器实现。由于Ocsid被仔细定义为使用PVS逻辑的类型和表达式子集，因此映射到相应的PVS声明和定义是相当简单的。由于确切的翻译模式对该方法并不重要，因此在此没有严格说明。下面显示了前面给出的简单示例视图映射的相关部分简单：理论开始C_ref：TYPE+C： TYPE =class[C_ref]x： TYPE =[[C，state] -> integer]A： ACTION = LAMBDA（st：STEP）： EXISTS（c1： C，c2： C）：guard（x（c1，now（st））=x（c2，now（st） ANDbody（（FORALL（ C_o：C）：如果C_o =c1，则x（c1，next（st））= x（c1，now（st））+ 1 ELSIF C_o =c2THENx（c2，next（st））=x（c2，now（st））ELSEx（C_o，next（st））= x（C_o，now（st））ENDIF））质量标准：质量标准=LAMBDA（b：行为）：FORALL（n：nat）：让st=（b（n），b（n+1））在A（st）或stutter（st）结束简单显然，从推理规范的角度来看，这种嵌入形式是可取的。每个动作直接对应于一个类似命名的函数，该函数对角色声明进行存在性量化。 实际的语义编码在身份函数guard和body中。因为视图是关闭的，所以它们会注意为所有类的所有对象指定操作的效果。浅嵌入的微妙之处在于处理绑定角色的动作体中的别名。J. 贺林/理论计算机科学电子笔记164（2006）61734.4连接嵌入由于我们已经描述了两个嵌入，现在我们必须连接它们的语义域，以便能够检查指定等价性。这一步是不可能的，除非它们共享一个共同的语义基础，在这个基础上构建两个嵌入。在这种情况下，嵌入已经被构造为共享未解释的类型STATE（显然还有BEHAVIOUR）。它们的关键区别在于结构和数据是如何表示的，即对象、值和变量。浅嵌入将这些规范映射到相应的PVS实体中，而深嵌入必须在 语言 级别 上管 理 它们 ， 在那 里可 以看 到 显式 类型 OBSIDLE ， VALUE 和VARIABLE。正是这两个世界需要连接起来，以比较Ocsid规范的不同PVS逻辑提供了一种类似于常规编程语言中的模板或泛型的理论参数化机制。我们使用这种参数化的fa-cility链接语义表示在深嵌入到他们的同行在浅嵌入。这部分地通过将包含深度嵌入的语义基础的理论主体中的适当声明移动到其理论参数列表来实现。这些变化如下所示。view_semantics[OBLOG：TYPE，var_map：[variable_syntax->[OBSTATE，STATE->VALUE]]，type_map：[type_syntax -> pred[VALUE]]，class_map：[class_syntax -> pred[OBLOG]]理论开始...端顺便说一句，关于连接的期望性质，当然有选择。在这种情况下，它可以在有关对象和值的不同处理的细节中看到。我们已经选择将数据类型VALUE提升到两个嵌入的共享语义基础，但使对象类型指定为特定的。这使得类型在结构上等价，而类在定义上是相互不相交的。为了在不改变深度嵌入的情况下支持名称等价，我们还需要使数据类型VALUE指定为特定的。然而，这种余地之所以存在，是因为我们故意将输入排除在深度嵌入之外。为了完成嵌入的连接，我们需要提供从一般理论实例化具体理论的参数为此，我们需要定义浅层实体的适当包装，并使用这些代理作为理论参数。这需要产生一个类型定义来包装指定的类。还需要生成将语法变量、类型和类包装并映射到它们的语义等价物的函数。下面是我们前面给出的简单视图示例。导入子句用生成的实体实例化视图语义理论。74J. 贺林/理论计算机科学电子笔记164（2006）61对象：数据类型开始c（cobj：C）：c？结束对象var_map（v：variable_syntax）：variable= IF name（class（v））=“C”THEN如果v = x_stx，则lambda（o：object，st： STATE）：如果c？(o)THENinteger_value（x（cobj（o），st））ELSEerror_valueENDIFELSElambda（o：object，st： STATE）：error_valueENDIF ELSE LAMBDA（o：object，s：STATE）：error_valueENDIFtype_map（name：nameid）：pred[value]=如果name=“integer”，则integer_value？ELSIF name=“boolean”THENboolean_value？ELSIF name =“C_ref”THEN（LAMBDA（vv：value）：reference_value？(vv)而c呢？(ref_val（vv）ELSE（LAMBDA（vv：value）：false）ENDIFclass_map（class：class_syntax）：pred[object]= IF class= c_stxTHEN c？ELSElambda（o：object）：false ENDIF导入视图语义[object，var_map，type_map，class_map]通过理论参数化，我们保持了两个独立嵌入之间的解耦性。唯一需要的更改是在深度嵌入中，我们需要使相关实体参数化。翻译工具有责任产生这种联系理论。5证明规格表示的等价性我们现在准备机械地证明，一个具体化的浅层和深层表示是相等的。对于这一步，有两种可能性。您可以使用定理证明器手动构造等价证明，也可以实现利用规范结构知识的证明生成器。我们首先讨论这些问题一般，然后提供从我们的例子规范的等价证明的亮点。J. 贺林/理论计算机科学电子笔记164（2006）61755.1非正式基础和动机等价性证明是高度系统化的，因为两个嵌入反映相同的这有助于实现证明生成器，使用户不必繁琐地处理语言的微小技术细节当然，这样的工具相对复杂，并且高度依赖于定义嵌入的证明系统。但假设有足够的用户基础，这将是更可取的，因为构建工具所花费的时间将在所有进行的等价性证明中摊销。简化等价证明的一个重要因素是保持规范的两个表示之间的结构相似性。当我们考虑跨句法转换的等价性在浅层情况下只要我们只使用定理证明器逻辑的可执行子集在深度嵌入中实现这些转换，我们就可以使用地面评估器来制作最终的深度嵌入版本。如果工具正确，两个嵌入的结构是相似的。重要的是要注意，在自动化的情况下，我们最终不会有关于证明生成器的新证明义务如果一个定理证明器可以成功地执行一个证明脚本到结论，我们不需要考虑脚本的来源，而只需要相信定理证明器。因此，无论我们是否手工证明，情况都不会改变。如果一个证明生成器总是失败，因为它生成错误的证明，那么它就没有价值。然而，如果它在普通情况下进行工作证明，它确实有价值。此属性适用于语言和工具的增量开发。在第一阶段，用户可以手工构造等价性证明。然后，编写一个粗糙的证明生成器，它可以处理最简单和最常见的语言结构。当项目达到合理的稳定性和需求时，最终的支出可以扩大到填充，以支持更深奥的结构。最后，如果我们要比较实现证明生成器和正式验证浅层翻译器之间所需的专业知识，我们会看到有很大的不同。前者需要传统的软件工程技能，而后者需要相当大的数学能力，正式处理复杂的编程语言结构。我们强烈地感觉到，在大多数情况下，验证几乎是不可行的，而提倡使用两个嵌入和证明生成器可能是可行的。5.2示例等价性证明为了使事情更具体，我们选择了为前面显示的示例说明提供等价性证明的选定部分。由于等价性证明需要处理大量的微小技术细节，即使是简单的规范，也不可能显示完整的证明树。幸运的是，这些证明的系统性允许选择的亮点来沟通所涉及的推理的解释者。76J. 贺林/理论计算机科学电子笔记164（2006）61PVS证明系统是基于证明演算的，它需要根据一组证明规则转换一个证明，直到得出结论或失败是明显的。对于我们的等价性证明，在证明树的根处，我们有浅深等价。正如可以预期的那样，它指出，对于所有行为，两种表示的含义必须相互暗示。 证明开始与skolemization的行为和分裂的证明到子树的两个方向的影响。所示的证明是手动构建的，因为证明生成器仍有待于未来的开发。浅深等值|-------[1]FORALL（b：behavior）：sem（simple_view）（b）<=>simple.SPEC（b）在第一个分支中，经过skolemization，instantiation和simplification，我们有1.2。它通过枚举联合动作来显示规范结构的更多细节。 从本质上讲，如果某个深层行动得到了满足，那么在同一步骤中就必须有一个满足的浅层行动。当然，在这些证明中，它总是相应动作的浅版本。shallow_deep_equivalence.1.2{-1}（EXISTS（a：action_syntax）：member（a，（：a_stx：））ANDsem（a，（：c_stx：），（： x_stx：））（b！1（n！1），b！1（1+ n！（1））或sem（the_stuttering_action，（：c_stx：），（：x_stx：））（b！1（n！1），b！1（1+ n！（1））|-------[1]A（b！1（n！1），b！1（1 + n！（1））[2]口吃（b！1（n！1），b！1（1+ n！（1））接下来的两个子目标是在第一次分裂行动之后实现的，然后执行定义的扩展，skolemization，实例化和重写。所有这些步骤在智力上要求不高，只需要对深域和浅域之间的实体关系进行简单的基于结构的簿记。因此，他们很容易受到机械化。顺序1.2.1.1.1不复杂，说明了动作防护装置的含义A.表达式级别现在是可见的，并显示了为什么浅表示对于推理目的是优选的。在深层表示中携带的显式绑定需要反复扩展，并使证明丰富（env是空环境）。建立这个目标是一个简单的重写和命题简化的问题。J. 贺林/理论计算机科学电子笔记164（2006）6177shallow_deep_equivalence.1.2.1.1.1：[-1]v（sem（equal（var_ref（c1_role，x_stx），var_ref（c2_role，x_stx）），an_envWITH[（c1_role）：= obj！1,(c2_role）：= obj！2]，b！1（n！（1））|-------[1]guard（x（obj！1，现在（b！1（n！1），b！1（1 + n！1)))为x（obj！2，现在（b！1（n！1），b！1（1 + n！（1））））序列1.2.1.1.2陈述了作用体A的含义。图2显示了得出肯定结论的证明子树的图。证明过程是通过分裂和有目的的实例化来管理别名，然后进行标准推理。图的想法不是传达个别步骤，而是对所涉及的细节给予一些直觉。shallow_deep_equivalence.1.2.1.1.2：[-1]FORALL（obj：（class_map（c_stx）：（var_map（c_stx，x_stx）（obj，b！1（1+ n！1））=primed_value（（：assignment（c1_role，x_stx，加上(var_ref（c1_role，x_stx），intconst（1）：），b！1（n！1），an_envWITH [（c1_role）：= obj！1,(c2_role）：= obj！第2节）(obj，x_stx））|-------[1]如果C_o！1 = obj！1THEN x（obj！1，next（b！1（n！1），b！1（1 + n！1)))为1 + x（obj！1，现在（b！1（n！1），b！1（1 + n！1)))ELSIF C_o！1 = obj！2THEN x（obj！2，下一个（b！1（n！1），b！1（1 + n！1))) 为x（obj！2，现在（b！1（n！1），b！1（1 + n！（1））78J. 贺林/理论计算机科学电子笔记164（2006）61否则x（C_o！1，next（b！1（n！1），b！1（1 +n！1）=x（C_o！1，现在（b！1（n！1），b！1（1 + n！（1））ENDIF序列2.1.2.1.2.1.2.2.1.2显示了作用体A的另一个蕴涵方向证明这与相关的J. 贺林/理论计算机科学电子笔记164（2006）6179图二. 1.1.2.1.1.2的证明子树80J. 贺林/理论计算机科学电子笔记164（2006）61复杂性，但由于嵌入方案的变化而不同。例如，不存在与角色参与者上的分支相关的实例化，因为深度嵌入的语义按需产生变量值。shallow_deep_equivalence.2.1.2.1.2.2.1.2： [-1]IF obj！1 = c1！1则x（c1！1，next（b！1（n！1），b！1（1 + n！1）=1 + x（c1！1，现在（b！1（n！1），b！1（1 + n！1)))ELSIF obj！1 = c2！1则x（c2！1，next（b！1（n！1），b！1（1 + n！1）=x（c2！1，现在（b！1（n！1），b！1（1 + n！（1））ELSE x（obj！1，next（b！1（n！1），b！1（1 + n！1）=x（obj！1，现在（b！1（n！1），b！1（1 + n！（1））ENDIF|-------{1}IF（obj！1，x_stx）=（c1！1，x_stx）var_map（c_stx，x_stx）（obj！1，b！1（1 + n！1)) = sem（plus（var_ref（c1_role，x_stx），intconst（1）），an_envWITH [（c1_role）：= c1！1,(c2_role）：= c2！1]，b！1（n！（1））（var_map（c_stx，x_stx）（obj！1，b！1（1 + n！1))= var_map（class（x_stx），x_stx）（obj！1，b！1（n！（1））ENDIF我们现在已经讨论了等价性证明中更有代表性的部分，目的是表明这些证明不仅可以手工产生，而且可以自动生成。至于遗漏，我们忽略了口吃的处理，因为它缺乏其他动作所没有的特征。我们还跳过了与实例化相关的类型条件的细节，因为这些都是通过确保决策过程有合适的类型谓词来处理的。如果我们考虑证明生成，很明显，复杂性在于准确预测应用证明步骤的结果。例如，当分裂时，我们需要能够预先确定结果的证明对应于哪个指定级别的子目标，以继续证明生成。幸运的是，如果不能静态地克服这一点，PVS提供了定义自定义证明策略的支持。他们有能力动态地确定业务特征并采取相应的行动。因此，我们可以定义证明策略来处理每个特定语言特定的证明子目标类型，并让它们相互调用虽然是通用的，但它们必须进行参数化，以接收有关手头规格的相关信息。