论文部分内容阅读
程序验证是计算机程序设计领域的传统研究课题，也是当前非常热门的可信计算研究的重点方向之一。然而，对于常见的绝大多数程序而言，完全正确性验证还是非常困难的。
程序的部分正确性和终止性是程序验证中两个重要的研究内容，得到了大量关注和广泛研究。研究程序的部分正确性主要的方式就是计算程序的不变式。循环不变式在程序验证领域发挥着不可替代的作用，它不仅是传统的归纳断言法的基石，而且在目前流行的很多软件验证技术中扮演着非常重要的角色。然而，循环不变式的自动构造技术一直是一个巨大的挑战。程序终止性是不可判定的。但是，很多具体程序可以通过严格的数学方法证明其终止性。
因此，本文对程序的循环不变式计算和程序的终止性证明进行系统、深入的研究，主要工作包括：
(1)对于循环程序的部分正确性，本文基于代数变迁系统理论通过不变式技术来进行验证。首先把待验证的循环程序转换为一个代数变迁系统，再根据程序循环体内的变迁关系，预先设计一个参数化的多项式模板集合作为预选不变式，依次从模板集中选取模板与初始条件和变迁关系分别组成一个多项式组。通过分别计算这两个多项式组的Dixon结式，从而获得该循环不变式模板必须满足的初始约束条件和连续约束条件，最终得到全局约束条件。通过对全局约束条件求解，进而得到具有该模板形式的循环不变式。根据模板的不同形式和约束求解的结果，最终得到不同形式的循环不变式，包括线性的、非线性的循环不变式。在对全局约束条件求解时，如果所对应的齐次线性方程组的解不唯一，则获得一组多项式方程共同构成一个合取形式的循环不变式。同时，这种循环不变式生成方法对于单分支和多分支的循环程序都是适用的。
(2)本文根据设计不变式模板集的一般方法所构造的模板项数太多，造成约束求解效率低下的问题，提出了一种启发式的设计模板方法，降低不变式模板的规模，提高了发现循环不变式的效率。
(3)对于验证循环程序的终止性，本文采用有限差分法来进行分析。虽有文献提出了验证循环程序终止性的polyranking方法，使用有限差分树来对一类多项式循环程序的终止性做出定性的分析。但是，对于循环程序的循环条件表达式与其差分值之间的关系，没有做深入的分析。本文使用有限差分法在循环条件表达式和其各次差分值之间建立起了联系，并且给出了严格的证明。从而，我们不仅能够分析循环程序终止的定性行为，而且能更深入地分析循环终止性的定量行为。在此基础上，解决了具有这种行为特征的多路径、非线性赋值的循环程序终止性判定问题。