《理论计算机科学电子札记》58卷第2期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html21页机械软件验证：从用户角度看Wolfgang Goerigk1;2InstitutfurInformatikundPraktischeMathematikChristian-Albrechts-Universitat德国基尔摘要我们目前的经验教训，从使用机械定理证明的证明支持软件验证，与可信的程序执行铭记。我们将使用两个实际运行的例子，编译器验证，这是中央，如果我们想证明，我们可以信任的一块可执行的软件，和一个工业项目中，我们证明了安全关键的专家系统使用（验证）运行时结果验证的正确性。我们将强调部分程序正确性及其保持的作用。我们将对高级控制方面进行评论，特别是对于一个具体的可执行软件，我们可以证明什么，我们不能证明什么。1引言我们的论文是关于软件验证的，即，关于证明我们想要保证的程序的属性，以便在程序执行中信任。但是我们如何机械地验证可执行的机器程序呢？我们是否能够证明现实可执行机器程序的非平凡正确性，并使用定理证明器进一步检查证明？或者我们应该更好地将这些尝试转移到维特根斯坦的逻辑怀疑论领域，认为任何推理方式都不会导致令人信服的解决方案|所以就放弃了？答案是否定的，我们有解决办法。但是，由于我们肯定不会成功地验证大型程序语义上的机器代码级别（至少不是在工程风格），我们必须模块化的问题。因此，我们的论文是关于源代码级验证的程序和编译器验证。1 电子邮件地址：wg@informatik.uni-kiel.de2 这里报告的工作得到了德国研究共同体（DFG）在Veri x和VerComp项目中关于正确的制造商和制造商实施验证技术的支持c 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。格里克2尽管存在上述问题，但很有可能公式化的定理根本不正确，或（实际上）不可证明，或无用。因此，一个主要的目标将是展示我们可以和我们不能期望能够证明一个现实的可执行软件。我们将强调部分程序正确性的重要性（参见。[22][23][24][25][26][27][28][29]对机器可执行程序的定期计算的非错误结果这通常是非常有效的，非常实用的，有时令人惊讶地容易证明，甚至严格，正式和机械。我们不相信一个令人信服的软件正确性证明所需的全部工作可以是“按钮”，即，全机械自动的。我们必须考虑证明什么以及如何证明它，这些任务与成功管理软件工程过程的任务非常相似。我们必须分析需求，考虑证明的架构和设计，最后我们必须使用特定的定理证明器来实现它们。为了说服我们的客户并帮助他们相信形式化和证明，需要额外的工作来制作一致和完整的证明文档。如果我们不想在机器码级别上验证程序，我们必须信任编译器。它们的可执行实现必须保证源程序的正确性属性被保留，以便我们可以信任生成的目标程序的正确性。但请注意，这为编译器及其实现打开了一个类似的问题，这是一个我们想要信任的（可执行）软件。为了避免cir-culi vitiosi，即，永远不会结束对不安全的可执行软件的依赖（不确定的血统，[21]），出于原则原因，我们需要一些手动验证检查。幸运的是，我们可以将这一工作完全推进到编译器实现正确性证明中，并严格验证编译器可执行文件，以保持源程序的适当和合理的正确性[17]。我们希望在源代码级别和编译器的正确性证明所提出的模块化。为此，我们使用两个t在一起的例子。在第2节中，我们概述了一个验证安全关键专家系统的工业项目。它的正确性证明实际上已经被ACL 2定理证明器检查过了[24]。安全性可以通过我们称之为（veri-ed）运行时结果验证[13]。 在第3节中，我们非正式地收集要求-实际的正确编译。第4节将产生一个数学框架，它使我们能够精确地定义NE编译正确性的preservation的源程序的正确性。特别地，我们将在ACL2（第5节）中为玩具编译器绘制部分正确性保留的机械证明。为了最终取得成功，玩具例子的作用至关重要，我们将在第6节中给出一些评论。最后，我们将总结一些经验教训，并对软件验证中使用的定理证明器提出一些希望。格里克32已验证测试结果验证证明大型软件系统的正确性这一任务似乎常常是不公正的。为了成功和高效地解决复杂的问题，启发式和编程技巧是必要的。然后，数学归纳法经常失败，因为要验证的算法变得过于复杂和棘手。这尤其适用于以知识为基础的系统。但是，如果这样的系统是安全或任务关键型的，我们依赖于它们的正确性。在[13]中，我们提出了一种基于检查器的软件验证方法，该方法利用了运行时结果检查[4]的思想进行验证。如果应用程序的部分正确性满足要求，则可应用。部分正确性可以通过后验运行时结果验证来证明。让我们勾画一个工业软件验证项目[3]，其中我们利用验证运行时结果验证技术（基于检查器的程序验证）来证明安全关键专家系统的正确性（可靠性）。该系统被称为Relais Master[1，25]，并且它是用于计算控制铁路系统的继电器组件组的测试计划的专家系统。它用于此类设备的工程阶段，以便（更自动地）为硬件在环测试提供支持。测试计划是从电路描述中生成的。之后，测试机器人将自动执行这些测试，以检查设备的正确电气行为。虽然数字电路在今天得到了更频繁的使用，但至少许多德国铁路系统仍然由继电器块控制。为了保证足够高的安全水平，这些设备需要定期维护，特别是需要在定期时间间隔内对每个物理设备进行重新认证。2.1Relais Master酒店|安全关键AI工具Relais Master可自动执行耗时且容易出错的手动测试计划构建。该系统由德国DTK公司（汉堡）与德国汉堡大学的人工智能实验室（LKI）合作开发。扫描电路后，工程师将其转换为内部图形表示，然后系统生成设备终端触点之间的一组测量值（测试计划）。每个测量都增加了有关继电器触点所需状态（断开或闭合）的信息。测试机器人稍后将自动切换继电器。我们对生成的测试计划有以下它应该是完整的电路，即，包含检测器械中任何数量缺陷的任何组合所需的所有测试（完好性）。它应该是“好的”，在这个意义上，它不需要太多的继电器切换操作，因为维护间隔主要是由估计的开关数量（质量）触发的。格里克4第一个属性是安全相关的，而幸运的是，第二个属性不是，尽管它对于实际可用性同样重要，并且使得AI技术的使用足以解决问题。但为了安全起见我们只需要平静。事实上，这种观察对于我们基于检查器的方法是至关重要的：对于给定的测试计划，可以很容易地检查可靠性，而测试计划生成是复杂的，并且还必须确保质量R1R2R34Fig. 1.样本电路。继电器R1有两个触点c1和c2，R2有触点c3和c4。如果R 1未被激励（释放），则触点c 1闭合（即，是导通的），而C2是开路的（即，隔离）。拓扑连接器是从布线和焊接中抽象出来的，对于n个端口，至少有n1个连接必须导通。Relais Master的输入是一个电路描述，实际上是从扫描的电路平面图手动构建的。图1显示了一个非常小的示例。内部面向对象的RelaisMaster数据结构的Ascii表示是以下形式的Lisp-s-表达式(((R1已释放（（c1关闭）（c2打开））（R2释放（（c3关闭）（c4关闭）（R3释放（（c5开）（R4释放（（c6开）t1t2t3t4）((t1c1）（t2 c6）（t3 c2 c4）（t4 t3 c2 c 4）（c1 t1 c3）（c3 c1 c5 c2 c4）（c5 c6 c3 c2 c4）（c6 c5 t2）（c2 t3 t4 c4 c3 c5）（c4 t3 t4 c2 c3 c5））((cont3t4（）（R1R2R3R4））（cont3t1（）（R1R2R3R4））(iso t2 t1（R3）（R1 R2 R4））（连续3t2（R3 R4）（R1 R2））(iso t3 t2（R2 R3 R4）（R1））（iso t1 t2（R2 R3 R4）（R1））(con t3 t2（R1 R2 R3 R4）（））（iso t1 t2（R1 R3 R4）（R2））(iso t2 t3（R1 R4）（R2 R3））））第一个子列表包含触点和端子，第二个子列表是电路的图形结构（每个节点后面都有t1t3TCC11t4TC6TC2CR13C2R2C4拓扑连接器C5tc3c6tTC5t2R格里克5第三个列表是测量的集合T，它们是两个端子之间的导通（con）或隔离（iso）测试|例如在T3和T4之间|接着是由该组激励继电器和该组释放继电器以该顺序给出的特定状态。在下文中，C将指代电路描述（前两个子列表），并且T将指代第三子列表，即，测试计划。C表示继电器主机的输入，T表示其输出。C和T一起形成正确性谓词检查Q的输入，该检查Q旨在由检查T对于C是完备的充分条件的程序来实现。2.2正确性要求为简单起见，我们只考虑包含端子、连接器（电线、焊接点等）的继电器组和继电器触点作为元件。二极管、电阻器和电容器被省去了。生成的测试计划包括传导和隔离测试。但是请注意，继电器触点是继电器的一部分，因此不能独立切换，测试机器人只能在端子（外部连接器）之间进行测量。由于稍后的认证应该是自动执行的，因此生成的测试计划以及Relais Master是安全关键的。我们需要以下保证：物理设备的任何继电器触点、连接器或端子的每一个缺陷都将通过测试计划的至少一个测量来检测所生成的测试的组合必须确保，如果成功，每个单独的元素都被单独测试以正常工作，即，导通（端子、连接器和继电器触点）和隔离（继电器触点），如果需要的话。在这种情况下，我们称电路C的测试计划T是完备的。关键的一点是，这是Relais Master程序（简称R）的部分正确性要求：如果它成功地为给定的电路C生成了测试计划T，那么我们希望T是正确的。设P（C）刻画正则电路描述，Q（T）定义T对C是完备的.然后我们可以用Hoare-三元组形式化R的正确性要求fP（ C）g T：= R（C）f Q（ T）g：部分正确性要求是安全关键应用程序中使用的工具的典型要求。我们不需要证明工具永远不会失败，但我们希望保证任何给定的结果都是正确的，即，工具的部分正确性。表示其结果正确性要求的前置和后置条件。2.3验证结果-获得想法让我们假设一个变换程序y：=（x）（或简称）由输入x和输出的前置和后置条件P（x）和Q（y）指定格里克6y. 而不是证明部分正确性fP（ x）g y：=（x）f Q（ y）g程序本身的|也就是说， 如果P对x成立，并且如果在x上成功终止，结果为y，则Q对y成立|其思想是修改程序并添加拒绝不正确结果的检查器谓词。 也就是说，我们构造了后置条件Q的一个有效的算法公式检查Q，并证明了（checkQ（x;y）=true）=）Q（y）：我们把这种性质称为检查器正确性。现在是一个简单的练习来证明下面的修改后的程序0，它另外检查后置条件并拒绝任何不正确的结果，对于P和Q是部分正确的：fP（x）g y：=（x）; if：check Q（x; y）then abortQ（y）g当然，我们还必须保证，运行不会损坏检查Q。在我们的例子中，我们在x和y的ASCI I表示上运行单独的检查程序，根本不修改专家系统。2.4《圣经》及其验证为了利用运行时结果验证方法，我们只需要在电路C和测试计划T上构造（并验证）谓词检查Q，其检查T对于C是完整的，即，这保证了后条件Q（T）成立。因此，为了验证Relais Master专家系统，仍然需要证明这种检查Q足以保证Q，即，（checkQ（C;T）=true）=）Q（T）：我们证明，只有当T中的措施足以保证C中的每个接触ci都被单独测试为导通（如果它应该被关闭）和不导通（如果它应该被打开）时，检查程序才返回真。拓扑连接器的端子和单个连接可以看作是特殊的闭合触点。注意，为了安全起见，再次证明检查器的部分正确性是足够的，即，即使Q保持，检查器也可能失败。我们必须证明，测试计划T是完整的电路C，如果检查成功返回真的C和T。我们不能详细说明这个程序和证明。检查器是一个Lisp程序。输入是表示C和T的s表达式（如上面的示例）。C是每个元件都有节点的图，T是在继电器触点的给定状态下两个端子之间的一组导通或隔离测试。t1和t2之间的成功导通测试保证了一条导通路径（我们不知道是哪条），而成功的隔离测试保证了每条路径都被隔离。然而，在这两种情况下，这很可能是由于格里克7缺损 收银员进来了 五个步骤：(i) 电路表示C被变换成更方便的内部图形表示。(ii) T中的每个测试都被C中t1和t2之间的所有路径及其类型的集合所取代。(iii) 测试中每条路径的每个触点都增加了相应的应该状态（打开或关闭）。(iv) 假设所有的测试都成功，我们得到关于具体设备中路径（集合）的物理传导的真逻辑命题;简单的逻辑变换给我们关于单独测试的单个元素的真命题。(v) 最后，我们检查每个电路元件是否都经过单独测试。如果没有，检查器中止。该检查器是在Boyer/Moore定理证明器ACL 2支持的应用性CommonLisp子集中编写的[24]。关于检查器和正确性证明的更多细节可以在[3，2]中找到。 关键部分（步骤4）可以被看作是一个问题专用的重言式或模型检查[7，23]：根据生成的测量值集T进行的成功的硬件在环测试将保证一组与电路相关的逻辑公式（表示端子触点之间路径的导通或隔离）为真，并且我们的检查程序基本上检查特定的 公式p^t^K^TCn^^（ced^ ：copen）Ll=1Jj=1我我i=1(for所有p个端子、k个拓扑连接器和所有n个继电器触点）是该组公式的逻辑结果：如果闭合，则每个端子、拓扑连接器和继电器触点导通，如果断开，则每个继电器触点 如果是，则集合T对于给定电路是完备的，即，（The Nite Set）测试用例的测试对于器械的认证是足够的。测试结果验证[13，35]与程序检查[4]密切相关，我们的案例研究是测试安全关键设备领域的应用。然而，我们的主要重点是验证的检查程序，保证正确的测试用例生成器（Relais主专家系统）。与例如[20]相比，其中测试用例生成基于模型检查，我们的方法不依赖于专家系统本身中使用的特定技术。 经典的验证和模型检验可能在复杂（和大型）应用中的限制。 我们坚信该（已验证）运行时结果验证在某些任务关键域中按比例增加|不仅是为了安全，也是为了安全。 该方法与Necula的证明携带代码和证明编译器[32，33]进行了比较，但我们检查了正确性的充分条件，而不仅仅是必要条件。格里克8与Relais Master专家系统相比，该检查器是用ACL2 Lisp编写的中等大小的递归正确性谓词。证明了它的（部分）正确性，并用ACL2进行了机械检验。然而，为了保证我们可以信任通过执行检查的Relais Master生成的测试计划，我们必须证明安全性，即，部分正确性，对于检查器可执行文件也是如此。这将我们带到第二个正在运行的示例：编译器验证。3程序的可信执行程序是顺序转换程序。一个编译器把一个源程序2SL作为输入，有时它会成功地终止并返回一个目标程序m2TL。如果是这样的话，我们希望m与。 实际上，我们需要保证m是的正确实现。但这需要进一步的解释，我们将在后面详细讨论正确实现的确切含义（第4节）。然而，一个实用的编译器在大多数情况下都会失败。实际上，它几乎会在每个源程序上失败（几乎每个源程序都有精确的数学含义）。通常有很多任意大的源程序，而编译器将在具有硬资源限制的nite机器上运行。因此，考虑到在真实机器上的可信执行，我们不能希望能够证明编译器（可执行文件）在每个正确的源程序上都能成功。但是我们可以证明，如果它成功并返回一个机器程序m，那么m是的正确实现。 这种需求背后的直觉对许多其他转换程序也至关重要，比如证明检查器、模型或等价检查器、将资金从一个账户转移到另一个账户的批处理运行等等。我们接受失败，但我们不希望看到不正确的非错误结果[36]。事实上，这正是我们经常依赖的，仅此而已。在我们每天使用程序的经验中，我们观察到它们由于分段错误或总线错误而失败，例如由于内存不足，程序员错误，编译器错误或在错误的假设下滥用优化编译器。虽然非常烦人，但我们都生活在软件错误中，但我们都希望应用程序员，编译器构造器，操作系统设计师甚至硬件工程师能够足够明智地检测并发出任何此类运行时错误。未被检测到的错误可能会产生有害的后果，特别是如果它们是故意的，在这种情况下，我们将其称为病毒或特洛伊木马[9]。作为编译器构造器，我们不能减轻应用程序员证明应用程序正确的负担。我们不能保证不正确的源程序实现的正确性。实际上，我们必须在不了解源程序意图的情况下构造编译器。另一方面，编译器不能保留每个格里克9源程序的属性我们必须在用户、语言设计者和实现者之间协商一份合同，该合同涉及要实现的具体语言的具体描述、目标机器的具体描述、两者的定义，这些定义在数学上都是足够精确的，以便用户和实现者可以在没有争议的情况下就它们达成一致如果合同中没有提及，则所有投注均为无效3.1非正式要求让我们收集一些正确实现的现实概念的要求：它应该处理目标机器的资源限制，处理源程序语义的非确定性，允许优化，还允许非终止反应程序的可信执行，支持源语言的全递归和动态数据类型。我们通常认为源程序是它们的机器实现的规范，因此要求目标程序至少应该像源程序一样定义，因此能够计算每个源程序的结果。也就是说，我们需要规范的经典实现正确性概念，例如VDM [22]。另一方面，我们通常不希望看到目标程序执行计算出的错误结果。也就是说，每个目标程序结果都应该相对于源程序语义正确[36]。 如果我们总结这两个要求，目标程序应该至少能够计算源程序指定的每个结果最多计算正确的结果w.r.t. 源程序语义细心的读者已经意识到，一般来说，这两个要求是相互矛盾的。它们只在极少数情况下满足，在这种情况下，我们可以保证目标程序被定义当且仅当源程序被定义时，并且在不确定的源程序语义的情况下，我们甚至可以保证目标程序能够计算每个源程序结果。实现通常比源程序更具有确定性，定义更少。如果我们倾向于一个正确实现的概念，它对应于第一个或第二个直观要求，这取决于用户程序的应用领域。对于日常编程情况，对应于上述第二项的需求通常是适当的正确性概念。 它不需要对源程序进行良好的证明，即使源程序没有被格里克10Io真的对于这种情况，我们想提出以下论点：我们可以信任机器程序的执行，如果我们能保证部分正确-机器程序的正确性和足够的数学严密性。注意，这里的“be unkned "意味着不返回任何非错误的结果，即，或者在运行时出错时中止，或者根本不终止因此，我们对转换程序的直观的编译正确性要求是保证生成的机器程序的部分正确性，但我们还没有说为了能够给出这样的保证，我们期望源程序具有什么样的正确性。这个问题实际上开启了一个关于源程序属性的深入而微妙的讨论，我们希望保留或需要例如优化（见[31，17]）。只要我们不真正依赖于复杂的优化，或者目标程序的终止保证，部分源程序正确性是足够的，这意味着我们需要一个正确的编译器来保持部分程序正确性，这对于现实的编译器可执行文件来说也是足够的，有用的，可证明的 [15，17]。请注意，分别使用ACL2进行编译器验证的规范或形式化工作有细微的区别。其前身是《易经》。J Moore在[28]中证明，（Piton机上）的每个非错误结果也将由m计算（在FM 9001上），m比......更确定。这个概念对应于上面的第一个直观要求，容易地允许优化，但是目标程序m的可信执行需要源程序的完全正确性证明。4转换程序让我们用部分关系（多值部分函数）fDi来建模转换程序的语义Do输入域之间Di和输出域Do. 因此f是一个元素f2（Di*Do ）=def2D i D o.Di和Do中的数据被认为是规则的或非错误的输入/输出数据或国家。为了处理不规则数据，即，夜间和夜间错误，我们假设每个数据域D由单独关联的不相交非空错误集，即，D=def D[D\=;.为每个转换程序语义f，我们假设一个扩展版本f2（D*D）我们用相同的符号f表示。错误是nal。任何计算都不能从错误中恢复.我们要以“以德待人，以礼待人”为己任。f是i和f（i）o的总和。3 错误不是我们意义上的错误。我们认为异常是非局部正则控制流的特殊情况格里克11我IoDOOOODtDt然而，我们必须尊重另一种现象。错误的类型基本上是不同的.它们要么是不可避免的，我们必须接受它们，要么是不可接受的，因此必须避免。实现必须保证可接受的错误被发送信号，因此不会导致意外的错误结果，而不存在不可接受的错误必须由用户证明，例如，如果她/他想要使用省略数组边界检查的优化编译器。我们将允许不可接受的错误造成不可预测的（或混乱的）后果。 为了模拟这一现象，我们划分在一个非空的集合A的可接受的和一个非空的集合U=defn A的una可接受的或混乱的错误。所以我们要求i=Ai [Ui和o= Ao[Uo以及f的强误差严格性，即f在i上是全的，f（A i）AO 和f（U i）U o：错误集应该包含一个特定的标准错误元素？ 这是在夜间计算中建模（发散）。我们还需要（d;？o）2 f无论何时有一个从d2D开始的f的非终止（nite）计算。4.1正确实施设f是源和f目标程序语义，并让2（D）*D t）s t ii i和2（D）* D t）是源和oo o目标输入和输出数据。我们需要两个关系，i和o，以及它们的在版本1和1中，是强错误严格的（在两个方向上）。fsS sIoIoIoft图二、源和目标程序语义fs;ft和数据表示i;o定义4.1（正确的实现或修正）ft被称为fs相对i和o以及相关错误集i的正确实现或修正（1）（i;f t）（d）（f s;o）（d）[A]对所有d2Ds成立，其中fs（d）Ds[As（即fs（d）\ Us=;）.i o o o对于任何一个目标程序计算，结果d00 inDt是A t中可接受的错误输出，或者存在以（常规）d0结束的源程序计算 对应于d00 或者以单位为Us的不可接受的（混乱的）误差输出结束。 也就是说，如果f t是一个正确的D格里克12DDi o io我SOSfs的实现，那么ft要么返回一个正确的结果，要么返回一个可接受的错误，或者，如果fs可以计算一个不可接受的错误，ft可以（混乱地）返回任何结果。如果ft正确地实现了fs的相对i和o，我们将写为i;ft wfs;o或更短的ftw fs（用黑体w）。我们用图3中的图来表示这个图的交换性，我们可以很容易地证明，fsfs 2Sems：ioIof2扫描仪：DtDtt tioft图3.第三章。 表示正确实现的交换图在垂直和水平方向上都能正确地绘制实现图。正确的实现是组合的，这对于实际的软件工程是一个非常重要的事实，特别是对于编译器的构造和引导（详见[17]这是一个重要的观察，我们可以通过保持相对正确性来准确地描述正确的实现[37]，这推广了Floyd和Hoare的部分和全部程序正确性的概念。 设f2（D*D ）是一个程序语义，让PD 和QD是谓词，即，常规数据的子集。f被称为相对于（前置和后置条件）P和Q（相对）正确，简称为i（2）f（P）Q[A o每当f以前置条件P成立的输入开始时则它或者以完成后置条件Q的输出终止，或者以可接受的错误结果结束，例如像重新呈现机器资源违规的状态。下面的定理说，ft正确地实现了fs，当且仅当fs的相对正确性对于所有的前置和后置条件P和Q都蕴涵着ft的相对正确性。在[17]中可以找到一个证明，在那里我们也讨论了这里定义的概念的一些变化。定理4.2（相对正确性的保持）fs（i;ftwfs;o）当且仅当对于所有llPDs和QDs，有hPifshQi=）hi（ P）iftho（Q）i：相对程序正确性推广了经典的部分或全部程序正确性概念为了看到这一点，设f2（Di*Do）是原始的未扩展程序语义，Di和QDo 在...后的条件。f称为部分正确的w.r.t. P和Q（简称fPgfQg），如果f（P）Q，即，如果f成立：无论何时格里克13我O我OTLSLSLTL对于输入d2Di，前提P成立，如果f（d）D0被定义，则一个nyd02f（d）满足P条件Q. f叫做全c或rectw.r.t. P和Q（简称[P] f [Q]），如果f另外保证定义在任何d 2 P上，即， 如果f相对于r.t. P和Q与Domaindomff包含P（也就是说，如果另外domfP成立）。让我们选择特定的错误集A=Ai=AO=def fag和U=Ui=Uo=def 具有可接受误差元素和不可接受误差元素的故障u对于b个域 Di 和D o。因此，=i=o=def A[U. 注意？2 f a; u g. 我们现在可以考虑？可接受（a=？6=u）或不可接受（u =？6 = a）。在这些特殊情况下，扩展的fext的相对正确性等价于fhPifext hQi（）fP gfQg如果？=a被认为是可接受的，它相当于完全正确，如果？=u被认为是不可接受的：hPifexthQi（）[P]f[Q]：4.2部分正确性我们的正确（相对）实现的概念也概括了众所周知的实现正确性概念。如果我们考虑？在我们的特殊情况下，（三）ext;fextwfext;ext（）i;ftfs;oi t so完全表示部分程序正确性的保存，如果我们考虑？另一方面，不可接受的，那么相对正确性的保持就等同于完全正确性的保持（详见[17]）。特别是，如果我们回到我们前面的评论，如果我们想要信任目标程序执行，并且如果我们不依赖于复杂的优化，则部分程序正确性的保持通常是有利的。它给我们一个数学上严格的保证，目标程序计算出最正确的结果。因此，部分正确性的保持（[12，30，29]或L-模拟[5]）是一个实际激励的适当特殊情况，并且根据上面的（3），我们可以很容易地使用未扩展的（部分）关系语义表示如下：定义4.3（L-模拟）设和m表示源和目标亲。语法与语义[]2（D）SL*DSL ）和[[m]]2（DTL*DTL），分别 然后我们说实施步骤七！m保持部分正确性（或mL-模拟），当且仅当（四）i; [[m]][[]];o：也就是说：如果目标程序m被定义在表示上，如果源程序的输入是常规的，那么源程序可以返回一个格里克14DDTLSLS不也是相应的结果。如果和因此m是确定性的，这意味着将返回相应的结果。[[ ]]SL 2SemSL ：i我[[]]SLSOO[[m]]TL 2SemTL ：ito[[m]]TL见图4。表示部分程序正确性从定理4.2可以清楚地看出，部分正确性的保持等价于前面定义的L-模拟推论4.4（部分正确性的保持）实现步骤7！m保持部分正确性，当且仅当mL-模拟，即，8P;Q： （fPgfQg=） fi （P）gmfo （Q）g）（）i; [[m]] [[ ]];o相对正确性的保持给了我们必要的手段去-正确实现的新的和更详细的概念也用于现实的正确编译，不仅保留部分正确性，而且用于优化编译器，其中目标程序输入必须满足所有额外的优化（总正确性）条件（不导致特定的运行时错误），以使目标程序可靠地运行[17]。我们可以将前一部分与通常的软件工程过程的需求分析进行比较。我们甚至可以称之为编译器正确性证明工程中的需求分析。其结果是一个数学框架，它允许我们精确地和正式地表达我们必须证明的定理，以便调用编译器正确。第5章证明编译器源代码级别的正确性现在让我们给出一个例子，并通过一个具体的编译器源代码级别的正确性证明，我们机械地运行了Boyer/Moore定理证明器ACL 2[24]。在[9，10]中，我们证明了Lisp编译器的部分正确性保持，我们想对源语言和目标语言，编译器及其正确性证明给出一个草图和一些简短的评论。在[9]中，我们定义了一个抽象堆栈机，以及一个为ACL 2的一个小子集生成堆栈机器码的编译器。编译器是用它自己的源语言编写的，这样我们就可以在ACL 2中执行它，要么直接作为ACL 2函数，要么在编译后（编译成抽象机器代码）通过执行机器模型并在其上运行编译后的编译器（机器）程序。后者模拟了ACL 2中编译器可执行文件的机器执行DD格里克15SLTL[9] 一直在那种（机器）程序上执行。我们实际上正式和严格地证明了源代码级验证不足以保证编译器可执行文件的正确性和可靠性。编译器正确性证明是最新的ACL2发行版的一部分，在[10]中有详细描述。源语言SL是ACL 2 Lisp的一个子集，类似于[26]的一阶相互递归函数的语言L3，但使用s-表达式s2SExpr作为（动态）数据。一个程序是一个函数定义的列表，后面是一个 输 入 变 量 的 列表和一个主程序表达式。（operational）semantic [[]]2（SEPr ！ SExpr）由ACL2函数求值，在将输入绑定到输入变量之后，将输入值（确定性地）映射到主表达式添加了一个终止参数（自然数n），以便在全递归函数的ACL 2逻辑中对严格部分函数进行建模（请参见[10] 了解更多详情）。目标语言TL是抽象堆栈机的代码。它的配置由一个代码部分和一个单独的状态栈组成，状态栈是一个包含Lisp s表达式的数据栈。该机器有六个机器指令，包括一个子程序调用和一个结构化条件。机器程序（m）是（相互递归的）子程序声明的序列（d）连同将在以下时间执行的主指令序列一起：将声明列表下载到代码中后的初始堆栈。的semantic [[prog]]2（SEPr！SEPr）的机器程序是一个堆栈-通过逐步执行机器指令来定义的变换。 它是德-由ACL2函数execute调用，该函数在初始堆栈上执行程序prog，该初始堆栈应该在顶部包含输入值再次，添加一个终止参数n，以迫使机器在最多n次子例程调用后停止执行。编译器编译程序是用SL本身编写的。它根据堆栈原理生成堆栈机器码，即， 在堆栈上传递参数，并且将给定的表达式e编译为机器指令序列，将e的值推到堆栈上，使下面的堆栈保持不变。函数或操作符使用（弹出）它们的参数并推送结果。（s1; ：;sn）2SEPr（评价n）的SEPr3s到你到你（sn; ：;s1; ：）2Sexpr（执行mn）Sexpr3（s;：）图五. 编译程序保持部分正确性;数据表示关系tos将s表达式（或s表达式列表）与包含顶部的s表达式（列表）的目标机器堆栈相关联（以相反的顺序）格里克16我们证明编译程序保持部分正确性（图5）。这个证明是由ACL2机械检查的，完整的ACL2证明脚本是最近的ACL2发行版的一部分。对于那些熟悉ACL2的读者，让我们引用[10]中的主要定理定理5.1（ACL 2中形式上的编译器正确性）（定义程序的编译器正确性(let（（new-stack（execute（compile-program prog））（append（rev inputs）old-stack）n））（value（car（evaluate prog inputs n）（implies（and（wellformed-program prog））（defined new-stack）（true-listp inputs）（equal（len vars）（len inputs）（equal new-stack（cons value old-stack）如果源程序是格式良好的，并且如果目标程序（应用于顶部包含以相反顺序的正确数量的输入的初始堆栈）在顶部返回非错误结果（被定义），则该结果等于应用于输入的程序的语义（评估）证明的关键部分是证明表达式编译的正确性上述程序的正确性定理，经过一些技术引理，是正确表达式编译的类似定理的简单推论，适用于程序的主表达式。 为了正确的表达式编译，我们证明两个定理同时归纳。第一个是形式（或表达式）的正确性定理，第二个是形式表的定理。他们两个非常相似。非正式地，对于格式良好的程序中的格式良好的表达式和表达式列表，我们证明：如果在编译的表达式（列表）上执行的机器被定义在n的堆栈上，则以下三个公式成立：(1) 表达式（列表）的语义|在给定的函数环境中，自由变量绑定到当前堆栈帧中的值。|对于相同的n，(2) 机器返回一个新的堆栈，表达式的值位于顶部（以相反的顺序），并且(3) 结果值下面的堆栈保持不变。证明实际上是对终止论元n和表达式的结构深度的计算和结构归纳的结合(in ACL2术语，这是一个有根据的归纳序数）。归纳是由一个大的可接受的ACL2函数提出的，该函数明确列出了我们成功证明所需的整套归纳假设。我们要证明很多引理。他们中的大多数是技术性的，但有些人反映了关键的见解，需要找到证据。例如，它是一种...格里克17休息，我们实际上必须证明的dennedness的源代码se-mantics和正确的结果，机器执行的同时。原因是有条件的。条件的确定性归纳地依赖于条件的值。条件不需要在两个选择中都是严格的，并且例如在递归定义中也不需要。条件句实际上是一个具有挑战性的案例，nd证明，而不是读者可能期望的函数应用函数的应用仅仅是通过计算归纳来捕捉的，而条件在很大程度上对证明结构有着至关重要的影响。但我们不想进一步详述。我们参考[9，10]。6论玩具的影响力从某种意义上说，我们上面的例子是一个玩具的例子相比，为实际的源编程语言和真正的目标处理器的现实编译器的验证所需的工作[17]。 我们的源语言非常小，抽象的目标堆栈机器代码是不切实际的抽象，远离现实世界处理器的丑陋现实。在这个意义上，[10]只是一种练习。但证明是一个有趣的练习，它在两个重要方面有助于实际的编译器验证：它可以通过后续编译阶段的机械验证来实现，例如（b）对具有线性堆存储（数据恢复）的堆栈机器，（c）对线性汇编代码，以及（d）对具体处理器的实二进制机器代码[15]。在正确编译器的Veri x项目[12，15，18]的背景下，该证明已被推广到更大的命令式源语言的部分正确性保留的机械PVS [34 ]证明[6]。步骤（b）的正确性已经人工证明，机械证明也接近完成[11]。步骤（c）和（d）被实现[15，16，14]并被设计为保持部分正确性。因此，除了是一个很好的练习之外，我们的证明可以被看作是中到大规模证明的一部分，以提供一个初始的完全验证的编译器可执行文件，该编译器可执行文件保留部分源程序的正确性[15]。在PVS证明中，我们使用结构操作语义和归纳关系来形式化部分函数。有趣的是，我们基本上可以重复使用这里给出的ACL2证明的证明思想和整体证明结构：PVS证明也是通过组合结构和计算归纳。在我们看来，这是一个关于证明工程的好消息在这两个方面，我们都受益于玩具的例子。它表明这样的证明在原则上是可管理的，没有过早地引入现实的复杂性;它实际上是保存的第一个机械证明部分正确。这样的证明是必要的，以提供二进制编译器正确性的数学严格证明格里克18可执行文件。事实上，后者是Veri x编译器正确性项目的最初动机：如果我们引导编译器，我们需要保证生成的编译器可执行文件的部分正确性。 我们需要 处理目标机器的硬资源限制，并支持源语言的完全递归和动态数据类型。7结论软件验证是可以成功的，尽管它通常被认为是困难的，甚至是不可能的|特别是对于大型和复杂的系统。机械证明支持可以帮助nding证明（和错误）。它可能有助于重做（或重用）证明后，轻微的修改。它可以证明正确性。但在后一种情况下，我们依赖于证明者。其积极成果，即，成功的否则，我们将在正确的软件构造和证明文档的机械支持过程中留下严重的空白。因此，我们也有一些愿望，特别是关于证明的可检查性和直观的建模：首先，为了说服我们的客户，不仅需要机械证明最终成功。一旦这样做，证明者还应该有助于一致和完整的证明文件。如果证明不能被可信任的证明检查者机械地检查这与编程非常相似：程序最终运行是不足够的。如果是这样的话，我们还需要文件。我们需要知道并沟通原因。第二个愿望有点技术性。编译器验证处理编程语言语义，并且程序通常意味着部分函数。在ACL2中，我们通过误差严格全函数对它们进行建模，这是一种繁琐的，并且总是需要额外的调整。同样，在PVS中，我们使用归纳关系，这也是一个有点乏味的处理。在这两种情况下，我们都需要非正式的元论证来证明形式化。虽然我们知道这些问
我的内容管理
展开
