证明编译器生成正确代码的方法及实现探讨

理论计算机科学电子笔记190（2007）65-82www.elsevier.com/locate/entcs认证代码生成阶段Jan Olaf Blech1 Arnd Poetzsch-He Putter2德国凯撒大帝大学计算机科学系摘要保证编译的正确性是正确软件的重要前提。 代码生成可以是编译器中最容易出错的任务之一。实现可信编译的一种方法是验证编译。证明编译器为每次运行生成一个证明，证明它已经执行了编译正确运行。在一个单独的定理证明器中检查证明。如果定理证明者满足于证明一个人可以肯定编译器产生正确的代码。本文报道了建设编译器的验证代码生成阶段。 它是一个更大项目的一部分，旨在保证完整编译器的正确性。本文着重论证了证明编译方法在代码生成中的可行性，并重点讨论了实现和实际问题。原来证明的检查是证明编译的实际瓶颈。我们提出了一个证明方案，以克服这一瓶颈。因此，我们证明了编译器的代码生成阶段处理的小型程序关键词：翻译验证，认证编译，定理证明，Isabelle/HOL1介绍大多数软件系统都是用高级模型或编程语言描述的。但是，它们的运行时行为由编译后的代码控制。 对于关键系统中的软件，静态分析和形式化方法可以应用于源代码级别是非常重要的，因为这个级别更抽象，更适合这些技术。然而，如果我们能够建立编译的正确性，则分析结果只能结转到机器代码级别。因此，编译正确性对于关闭从高级形式化方法到机器代码级别的形式化链是必不可少的。可以区分两种一般方法来建立编译器3的正确性：1电子邮件地址：blech@informatik.uni-kl.de2电子邮件地址：poetzsch@informatik.uni-kl.de3我们遵循[11]中给出的概念，并根据Dagstuhl研讨会05311“优化配置器”中的讨论对其进行了稍微改进1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.00866J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65• 认证编译器：首先证明编译器的算法为所有给定的格式良好的输入程序定义了正确的翻译（编译器算法正确性），其次证明算法在给定的机器上正确实现（编译器实现正确性）。我们称一个编译器为机器检查证明这两个项目是一个认证的编译器（算法/实现）。• 认证编译器：提供一个证明（称为证书），证明目标程序是源程序的正确翻译，无论何时执行这种翻译。重要的是要注意，这些证明并没有说明算法或其实现，而只是说明两个程序的关系。不同的技术已经开发出自动生成这样的证明（见节。6）。与编译器证明相比，编译器证明其结果的技术有两个优点。首先，实现正确性的问题可以完全避免，也就是说，我们不必相信硬件系统上编译器算法的实现或证明它是正确的（参见。[19，5]在这个问题上。其次，类似于携带代码的证明方法（[14，13，1]），该技术在编译器生产者和用户之间提供了一个清晰的接口。在认证编译器方法中，编译器用户需要访问编译器正确性证明以确保其正确性。因此，编译器生产者必须揭示 编译器的内部细节，而翻译证书可以独立于编译器实现细节。认证编译器方法的缺点是用户必须检查每个（关键）编译的证书，如果编译器有bug，这种检查可能会失败我们已经构建了一个认证编译器，将C子集转换为MIPS [17]代码。我们的认证编译器框架在[5]中描述。它包括以下特点• 机器可检查性和逻辑的独立性：所有的规范和证明都是基于形式化的一般逻辑的机器可检查的，也就是说，一个独立于翻译中使用的语言和技术的逻辑。我们使用Is-abelle/HOL [16]作为我们的规范和验证框架。• 翻译契约：我们需要一个明确的翻译契约，正式指定源语言和目标语言的语义和翻译正确性谓词。• 认证编译器：我们感兴趣的是一种技术，编译器生成证明脚本作为可检查的证书。本文详细介绍了代码生成阶段的构建和扩展以及证书的检查。我们强调我们的方法的实际适用性。这尤其意味着要优化检查证书所需的时间。 本文的主要技术贡献是：• 介绍了我们具体的认证代码生成阶段。这包括J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）6567生成证书所需的扩展• 编译器生成的证书的结构和优化最大限度地减少了进行证明所需的时间。为了这个目标，我们区分程序独立的部分，每个程序必须执行一次的部分和程序中每个指令必须单独执行的部分。特别是，我们提出了一个解决方案，以证明更有效地正确证明一个映射函数的内射一次，使我们能够为每个程序，放弃程序中每条指令的复杂大小写区分• 实验结果、经验、验证假设和关于如何更有效地运行验证的技术建议。(To据我们所知，我们是第一个开发这种方法的原型实现的文件概述第二节描述了中间语言、生成的MIPS机器码以及它们之间的关系。代码生成算法和验证正确性的证明在第3节中描述。第4节描述了认证过程的自动化和性能增强。第五节，我们对自己的工作进行评价。第6节讨论了相关工作，第7节得出结论。2语言及其语义等价在这一节中，我们概述了我们的中间语言和MIPS语言的语法和语义，以及它们之间的语义等价性。 本节建立在[5，19]中提出的工作基础上。定义了中间语义和MIPS语义一小步一小步的操作。因此，我们将语法定义为抽象数据集，将状态定义为元组，将转换规则定义为nextstate函数。如果两个程序产生相同的输出轨迹，则它们在语义上是等价的.2.1中间语言中间语言的语法定义该语言包括（数组）变量赋值、表达式、条件和非条件分支、用于输出的打印语句和退出语句。程序是语句的列表。中间语言的语义如图2所示。它在Isabelle/HOL中被形式化为状态转移函数evalstatement。为了缩短演示文稿，它被稍微简化了。系统状态包括三个组成部分。第一个是迄今为止发生的输出序列，表示为列表。#表示将元素添加到列表中。第二个由一个程序计数器组成，该程序计数器索引程序的当前指令最后一个内存状态是从变量到它们的值的映射变量表示为整数元组。第一个组件对应于变量名。第二个参数表示数组的索引，或者表示原语的索引68J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65（（数据类型操作数=CONSTint |VAR整数|ARCONST int int |ARVAR int int数据类型表达式=运算符操作数|加运算元操作数|MINUS操作数|MULT操作数|LT操作数|LE操作数数据类型语句=ASSIGNV int表达式|ASSIGN AC int int表达式|ASSIGN AV int int表达式|BRANCH表达式int |GOTO int|PRINT int|出口Fig. 1. 中级语言课程evaloperand varvals（CONST c）=cevaloperand varvals（VAR v）=varvals（v，0）evaloperand varvals（ARCONST v i）=varvals（v，i）evaloperand varvals（ARVAR v vi）= varvals（v，varvals（vi，0））evalexpression varvals（OPERAND o1）=evaloperand varvals o1evalexpression varvals（PLUS o1 o2）=evaloperand varvals o1+ evaloperand varvals o2evalexpression varvals（MINUS o1 o2）=evaloperand varvals o1 - evaloperand varvals o2evalexpression varvals（MULT o1 o2）=evaloperand varvals o1* evaloperand varvals o2evalexpression varvals（LT o1 o2）=evaloperand varvals o1 evaloperand varvals o2<然后1其他0evalexpression varvals（LE o1 o2）=evaloperand varvals o1≤ evaloperand varvals o2然后1其他0evalstatement（outp，pc，varvals）（ASSIGN V v e1）=（outp，pc+1，varvals（（v，0）：=evalexpression varvals e1））evalstatement（outp，pc，varvals）（ASSIGN AC v i e1）=（outp，pc+1，varvals（（v，i）：=evalexpression varvals e1））evalstatement（outp，pc，varvals）（ASSIGN AV v vi e1）=（outp，pc+1，varvals（（v，varvals vi）：=evalexpression varvals e1））evalstatement（outp，pc，varvals）（BRANCH e1 lab）=evalexpression varvals e1= 1 then（outp，lab，varvals））else（outp，pc+ 1，varvals）evalstatement（outp，pc，varvals）（GOTO lab）=（outp，lab，varvals）evalstatement（outp，pc，varvals）（PRINT v）=（（varvals v）#outp，pc+1，varvals）evalstatement（outp，pc，varvals）（EXIT）=（终端#outp、pc、varvals）图二. 中间语言语义变量为了简单起见，我们只将无限整数视为语言定义中的类型。然而，在扩展版本中，我们也处理布尔值，这并没有使语义定义和证明变得太复杂。（J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65692.2MIPS语言MIPS语法的定义可以在图3中找到。在中间语言中，程序是指令列表应该注意的是，PRINTINT和PRINTKARRAYSIZE指令不是真正的MIPS指令。它们最多由三条实际指令组成，但出于简单起见，本文将其作为一条原子指令70J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65（（→→数据类型指令=ADD int int int |ADDI int int int |int int int |MLT int int int |int intint |SLTI int int int |SLE int int int |SLEI int int |STORE int int|LOAD int int|BGTZ int int|J int|PRINTINTint |KARRAYSIZE int int|返回图三. MIPS评估指令（outp，pc，pcs，pcs）（ADD r1 r2 r3）=（outp，pc +1，r1：=（r2）+（r3）），）evalinstruction（outp，pc，pcs，pcs）（ADDI r1 r2 c）=（outp，pc +1，n（r1：=（r2）+c），n）evalinstruction（outp，pc，pcs，pcs）（r1 r2 r3）=（outp，pc +1，n（r1：=（n r2）-（r3）），）evalinstruction（outp，pc，pcs，pcs）（最低限度r1 r2 r3）=（outp，pc +1，n（r1：=（n r2）*（r3）），）evalinstruction（outp，pc，pcs，pcs）（MLT r1 r2 r3）=（outp，pc +1，r2（r1：=（r2）*（r3）），r3）evalinstruction（outp，pc，r2，r3）=（correctstep ilprog tlprog PCIL PCTL（STEPS PCTL）VARMAP PCREL）”见图6。 程序等价准则用正确的值实例化。这些通常由编译器提供，并包含在证明脚本中。 如果编译器提供假值，则证明不会成功仿真关系要求可以在定义中识别。我们有一个初始的要求，即开始状态是在关系中（前两个元素的结合）。合取的最后一个元素形式化了模拟定义的步骤部分。它利用谓词correctstep确保 对于模拟关系中的每个相应的中间语言和MIPS状态，后续状态将再次处于该关系中我们已经介绍了一种中间语言和MIPS处理器指令的一个子集，以及它们的语义。我们还提出了语义等价的标准。请注意，我们的语义形式主义还不包括整数算术。这是MIPS机器的有限整数表示的一个抽象。因此，由于整数表示的大小有限而发生的错误不是本文的问题。 本文的重点是证明编译器方法的适用性，而不是所涉及语言的语义特征（参见例如[3]定义和推理更复杂的中间语言的语义的方法）。本文中使用的程序等价准则允许将中间语言操作转换为一个或多个MIPS指令的验证。对于我们的代码生成阶段，这样的（1：n）标准是足够的，也是简单的证明过程。然而，在其他编译阶段，必须使用其他标准（参见。[5]）。3代码生成阶段在本节中，我们描述了代码生成过程，该过程受本文所述的验证过程的影响。我们还勾画了一个一般的策略，以证明生成的MIPS代码的程序是语义等价的中间语言表示。J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65733.1代码生成算法在我们实现的代码生成器的第一步中，执行寄存器分配。它决定了变量的值是否应该存储在寄存器或存储器中。在我们的实现中，我们使用一个非常简单的寄存器分配算法，将寄存器中的前10个非数组变量和所有其他变量（特别是数组）映射到内存中。应该注意的是，我们的技术可以处理更复杂的寄存器分配模式。在下一步中，我们为非寄存器映射变量分配内存位置。这些步骤的一个结果是从中间语言变量到寄存器和存储器地址的映射（变量映射）。这种映射不仅在编译过程中使用，而且对于进行证明也至关重要。在下一步骤中，按顺序处理中间语言程序 并且为每个语句生成一个或多个MIPS指令。这种生成是通过简单的标准编译器教科书算法完成的。因此，对表示中间语言语句的每个指令代码序列进行了一些简单的优化.该阶段的副产品是相互对应的中间语言和MIPS代码程序点在最后一次通过MIPS程序时，借助于该程序点对应关系来解决跳转目标。这种关系对于正确性证明的进行也是很有帮助的整个编译器使用ML编程语言实现3.2编译正确性的证明为了证明代码生成运行正确，我们必须证明中间语言程序和生成的MIPS程序满足图6中的正确性标准。因此，我们必须证明这两个程序相互模拟。它们必须满足第2.3节中模拟关系的要求。• 我们必须证明这两个程序的初始状态是模拟关系。这是通过简单地展开等价标准定义来完成的。• 我 们 必 须证 明 ， 对 于 来自 中 间 程 序 和MIPS 程 序 sIL 和sMIPS 的 每 两 个 等价（ESTA）状态，后续状态再次等价：sILsMIPS=evalstatementsIL（ picstatsIL IL） evalN指令sMIPS（corstepsMIPSILMIPS）MIPS如第2节所述，evalstatement和evalN指令是状态转换函数。picstat从中间语言程序中挑选适当的语句。corsteps为中间语言语句提供相应的MIPS指令数。这一项的问题是，我们对sIL和sMIPS的信息很少，但它们是模拟关系，并且它们是一个特定的程序。 如果sIL，sMIPS是终端状态，这直接从我们的语义定义中得出（参见。EXIT和RETURN语义的定义74J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65第2节）。 如果程序没有终止，那么一定会有一些声明，接下来将在中间语言程序中执行。因此，我们对中间语言程序的所有语句进行了区分。模拟关系将该语句与MIPS程序中的机器代码指令相关联。 我们必须证明中间语言语句的执行导致与相应MIPS程序点的执行所达到的状态等价的状态。这种对给定程序的程序点的区分是证明中间语言程序与MIPS程序等价的关键。应该注意的是它是从另一个抽象状态中演绎出一个抽象后继状态，其规则定义了第2节中介绍的语义。 因此，这种采购提升了基于跟踪的语义的动态性质，以静态视图增强了在定理证明器中推理可能处于有限状态系统的可能性。4认证过程在本节中，我们将描述编译器生成的证明，以确保代码生成已正确执行。对证据的传导也进行了说明。我们还描述了编译器中必须为证书生成而修改的部分。在本节的最后一部分，我们将研究性能问题，也就是说，定理证明器用来证明我们生成的证明是正确的时间。我们展示了如何重组的证明原则，使检查更快。4.1证明的生成与实施在这一小节中，我们描述的生成的正确性证明和他们的自动传导Isabelle/HOL。每当编译器（代码生成）运行完成时，我们都希望进行正确性证明。我们要用不同的方法来证明不同的文件。包含翻译契约（所涉及语言的语法、语义定义和语义等价标准）的文件是独立于程序的，不能由编译器生成。同时还改进了其它一些性能增强特性，并生成了非编译器。具体证明由编译器生成，中间体（IL）和MIPS语言转储图7分别显示了编译器、代码生成阶段。以及编译器生成的理论文件及其依赖关系（虚线）。在我们的编译器中实现的代码生成阶段采用中间语言程序并输出MIPS汇编代码。此外，还创建了几个与Isabelle定理证明器一起使用的理论文件。这些文件是关于程序和编译过程以及子证明的事实的集合。在一开始，原始的中间语言程序被转换为Isabelle表示，并写在一个单独的文件中。同样，在MIPS大会结束J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）6575源ILILMIPS汇编代码前端IL优化代码生成IL MIPS程序表示法对应程序点（变量−>内存）映射翻译合同– 句法语义– 等效性标准验证：InjProof（variable −> memory）单射证明：步骤IL MIPS中的等效程序步骤返回等效结果校对：FinalProofIL MIPS程序图7.第一次会议。编译器和生成的理论文件具有依赖关系代码也被写入Isabelle文件还有一个文件，其中保存了中间语言和MIPS程序中程序点的对应关系以及变量映射。 这个信息无论如何都是在编译器中计算的（参见。第3节），并简单地写入伊莎贝尔文件。 请注意，它只对证明的进行很重要。 语义等价标准本身并不需要它。Finally InjProof.thy、Steps.thy和FinalProof.thy是包含正确性证明的文件。它们是由我们的认证编译器的一个特殊的证明生成器模块计算的，该模块独立于编译器的其余部分。该模块以中间语言代码和生成的MIPS代码以及对应程序点的关系和变量映射作为输入。生成的文件确实依赖于几个额外的非编译器生成的理论文件，这些文件包含翻译契约。出于性能原因，我们编写了大量的非编译器生成的预先证明的引理。这个集合目前包括70 lemmata。它们中的大多数执行相对简单的转换，例如将证明目标拆分为几个较小的证明目标或陈述一些通用的等式和含义。它们封装了在证明过程中经常发生的操作。FinalProof.thy包含最高的正确性标准。为了证明中间语言程序和MIPS程序的输出轨迹的语义等价，必须证明它满足2.3节中描述的语义等价的标准。在第一步中，定理证明器证明了初始状态处于等价关系。这是一个简单的任务，直接在Finalproof.thy文件中完成。下一个任务是证明对于每一对等价的状态，随后的状态再次等价。在实践中，这是通过在具体程序中的位置上进行大的情况区分来完成的，如第3.2节所述。在这些位置上执行中间语言和MIPS程序，76J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65抽象，即抽象而非具体的状态。 一个是表明所得到的态将再次处于等价关系。我们用独立的引理证明这些步骤，这些引理本身在Steps.thy中被证明是正确的steps.thy中的一个引理证明了每个相应的程序位置执行一个步骤是正确的。这是通过查看中间语言和MIPS程序的操作数和操作来完成的。 它们必须相互对应。如果变量映射是单射的，则语义等价的其余证明是相当容易且相对快速的。图8中描述了一个典型的编译器生成步骤，目的是让自动定理证明器Isabelle/HOL高效使用。这一步证明的第一部分是用引号表示的实际正确性引理。 我们必须从两个态的等价性（IL TL步等价性）中推导出两个后继态的等价性。 第二部分由引理的证明组成，本身就是一种由定理证明器解释的程序。 不同的策略被应用于行为证据引理指出，对数组变量的赋值是正确的。因此，如果数组索引在证明脚本开始时在数组的边界内，则区分大小写。 MIPS和中间语言的实际指令和语句不显示，而仅作为对列表的引用出现的指示/声明。在接下来的行中，程序步骤被符号化地评估，即，表示状态转换对原始状态的影响。作为一个公式。 在下一段中，状态等价的定义被展开（IL TL步当量）和不同的要求。第一个是证明被处理的指令是相互对应的。 然后证明了所得到的内存/寄存器值和变量值的等价性。这就是变量映射（MapFun m）的内射性（injtheorem）发挥作用的地方。因此，编译器在一个单独的文件InjProof.thy中证明了这个映射的注入性。 存储在MIPS代码执行期间出现的临时值在几个特殊的寄存器中，没有变量被映射到。4.2性能问题本节涉及我们的认证代码生成器及其Isabelle证明的性能问题。生成和执行证明所需的时间对于在工业和科学中接受认证编译器方法至关重要。我们提出的策略使证明的进行比我们最初的天真方法快得多。编译器内的证明生成所花费的时间在代码生成阶段中可以忽略不计。实际的代码生成器几乎需要线性时间，包括将Isabelle表示和证明写入文件的部分。然而，在Isabelle定理证明器中验证证明需要相当多的时间，减少这一时间是一项重要的任务。本节介绍我们实现的解决方案以及对它们的运行时复杂性的估计。在本节中，我们将使用|P|作为中间程序和MIPS程序中的程序指令/操作的数量。 |V|的数目记在J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）6577| |lemmastep16：“[|....IL TLstep equiv（ac IL，outp IL，terms IL，（16，varvals））RelVarSet（MapFunm）PCrel（ac TL，outp TL，terms TL，（44，memvals））|]===IL TL step equiv（evalstatement（ac IL，outp IL，terms IL，（16，varvals ））（ith ILprog 16））RelVarSet（Map- Fun m）PCrel（evalN instructions（ac TL，outp TL，terms TL，（44，memvals））（Suc（Suc（Suc（Suc（Suc（Suc（Suc（0））TLprog）apply（case tac<&apply（subst evalstatementsplitter，subst ILprog def，（ruleith1，simp（no asm），simp（no asm）+）？，simp（no asm），simp（no asm））应用（substevalNumbers splitter0|（substevalNumbers splitter1，（substTLprog def，（ruleith1，simp（no asm），simp（no asm）+）？，simp（noasm）），simp））+首选2apply（subst evalstatementsplitter，subst ILprog def，（ruleith1，simp（no asm），simp（no asm）+）？，simp（no asm），simp（no asm））应用（substevalNumbers splitter0|（substevalNumbers splitter1，（substTLprog def，（ruleith1，simp（no asm），simp（no asm）+）？，simp（no asm）），simp，（subst if not P，simp）？，(simponly：Let def））+应用（简单添加：IL TL步骤等效定义）适用（规则第s4ir条|规则S3IR|规则S2IR|规则s1ir）apply（simp（no asm）only：One nat def PCrel def set t1 set t1h1 set t1h1应用（规则插入定理）apply（simp（no asm）only：One nat def RelVarSet def set t1 set t1h1 set t1h1apply（simp only：MapFun def fun2at fun2atapply（rule opsplitterplus，（rule tac memvals=memvals in varconc，simp+，simp（no asm）only：RelVarSet def set t1 set t1h1 set t1h1apply（rule tac m=m and c=9 and MapFun=MapFun in dynarrayacc，simp，simp，simp（no asm）only：MapFun def fun2at fun2at' fun2bt，rule w100，rule tac memvals=memvals in varconc，simp+，simp（noasm ） only ： RelVarSet def set t1 set t1h1 set t1h1' set t1h0 ， simp （ no asm ） only ： MapFun deffun2at fun2at' fun2bt ， rule tac memvals=memvals in varconc ， simp + ， rule tac c=9 indynarrayacc2，simp，simp，simp，rule v100）？应用简单+完成图8.第八条。 生成一步证明变量我们将每个数组元素作为一个单独的变量。 A是程序中数组的个数。以下属性在我们的代码生成框架中保持不变：78J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）65• 由于Isabelle中的程序表示为指令列表，一条指令需要O（|P|）时间。J.O. Blech，A.Poetzsch-Heffter/Electronic Notes in Theoretical Computer Science 190（2007）6579| || |||• 在一组变量中查找一个变量以及在变量映射中查找一个寄存器/内存位置需要O（V）时间。我们使用一些简单的查找引理/规则来实例化Isabelle简化器策略，这些引理/规则禁止对集合和映射函数定义进行线性处理以实现此结果。• 程序计数器关系中元素的查找，即中间语言和MIPS代码中对应程序点的关系，可以在O（|P|）时间。• 如第3.2节所述，抽象模拟步骤的验证对于我们的正确性证明至关重要。由于Steps.thy中的单步引理的证明确实需要进行常数次的查找才能得到对应的-ing指令以及常数数量的查找，以获得相应的变量/内存/寄存器位置的步骤中的一个步骤。时间复杂度为O（P+V）。 然而，一个步骤只能证明正确的与此电子邮件如果变量映射的附加要求已经被预先证明。必须确保仅显示作为指令参数的变量/存储器/寄存器位置。这意味着，我们必须要求，如果写入对应于中间语言变量的MIPS存储器位置，则对应于另一存储器位置的存储器位置不会改变。因此，我们必须要求变量映射是单射的。 第二个要求对阵列地址的对齐进行了限制。这些任务在单独的证明中完成，每个程序只执行一次4.3映射函数性质的证明用归纳的方法证明了变量与存储器/寄存器位置之间的变量映射的单射性。这意味着：我们证明了一个映射与一个变量和内存/寄存器的位置是单射的。通过添加额外的变量，我们证明了包含额外变量的映射到新的内存位置仍然是内射的。 为了以简单的方式做到这一点，我们使用记忆计数器所有先前变量的内存位置都低于此内存计数器。因此，如果我们分配一个新的内存位置，并且它等于或大于这个计数器，那么所得到的映射将再次是单射的。 该证明与第二个是一个属性，该属性对于将数组地址解析为内存位置至关重要。下面描述用于证明映射函数性质的内射性的模式• 对于每个新的变量映射，我们证明一个引理：利用之前没有变量映射到某个地址以上的存储器位置以及实际存储器位置映射到该特定地址的事实，我们证明映射仍然是单射的。这需要O（1）时间。 我们还证明了没有内存位置映射到这个（某个地址+4（整