【作者】 武斌；

【导师】 杨路；

【作者基本信息】 华东师范大学 ， 系统分析与集成， 2010， 博士

【摘要】 程序验证是计算机程序设计领域的前沿研究课题,如何保证程序正确性是计算机科学的一个重大挑战.近年来,随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求,使用符号计算理论来解决程序验证中的相关问题被认为是一种有效途径.本文利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成.循环不变式在程序的部分正确性验证中起着非常重要的作用,如何生成循环不变式也是程序验证领域的挑战之一.本文主要研究了多项式循环程序的不变式生成问题.首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成,设计了一个多项式时间复杂度的循环不变式自动生成算法,可生成多项式等式型循环不变式.程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一.本文主要研究了一类带有非线性循环条件和线性赋值的循环程序的终止性分析问题.通过计算线性赋值矩阵的约当标准型,确定循环条件在循环次数充分大时的符号,将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问题.如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期,则这类非线性循环程序的终止性问题是可判定的.另外一个值得研究的问题是如何计算合理的前置条件,使得循环程序在满足该条件的前提下是终止的.本文基于一阶常系数差分方程组的求解技术,设计了一个高效、实用的前置条件生成算法.我们将程序的循环赋值语句转化为程序变量关于循环次数的差分方程组,计算差分方程组的闭形式解.然后将闭形式解代入循环条件,在循环次数充分大时,判断循环条件的符号,进而生成循环程序合理的前置条件.针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法.进而,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了相应研究.研究结果表明,符号计算是验证程序正确性的一种行之有效的方法.我们期待将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的有前途的验证工具.更多还原

【Abstract】 Program verification is one of the frontier research topics in program design field, which has important theoretical significance and application value. In this dissertation, we introduce some classical algorithms in symbolic computation into program verification, and mainly do researches on program verification in three basic aspects:generation of program invariants, termination analysis and generation of preconditions.Loop invariants play a very important role in proving partial correctness of pro-grams. we mainly study the invariant generation of polynomial loop programs. We firstly present a new method for generating polynomial invariants of polynomial loop programs by computing vanishing ideal of sampling points. A reliable polynomial time algorithm for generating polynomial invariants is established.Termination analysis of loop programs is very important in many applications, es-pecially in those of safety critical software. In this dissertation, we mainly study the ter-mination of programs with polynomial guards and linear assignments. The discussion is based on simplifying the linear loops by its Jordan form. And then the process to find the nonterminating points for general polynomial guards be reduced to semi-algebraic system (SAS for short) solving. If the number of functions in SAS are finite or the functions are integer periodic, then the termination of programs is decidable.However, instead of considering complete termination of programs, i.e., termination for all inputs, we are more concerned with the following questions:How if the code only terminates for some inputs? In this dissertation, a rapid and reliable algorithm for gener-ating preconditions of loop programs with linear or nonlinear assignments is established. Clearly, a loop program can be elegantly expressed by means of a system of difference equations, which describes the behavior of the loop variables changing at each iteration. The method is based on solving systems of difference equations corresponding to the loop assignments, and then substituting the solutions into the loop guards to compute precon-ditions that ensure the termination of the loop programs.The results indicate that symbolic computation is a valid tool for studying program verification. We hope that more and more classical algorithms in symbolic computation can be introduced into research on program verification.更多还原