程序正确性验证的代数方法及其研究进展  

A survey of algebraic methods for program correctness verification

作　　者：廖苑蓉[1] 陈光喜[1] 

机构地区：[1]桂林电子科技大学数学与计算科学学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2013年第1期49-55,共7页Journal of Guilin University of Electronic Technology

基　　金：广西可信软件重点实验室开放基金(KX201213)

摘　　要：程序的完全正确性包括程序的部分正确性和终止性,为了提高程序验证的正确性,介绍了程序正确性的验证方法,包括基于公理化验证程序的完全正确性,基于不动点定理、特征值理论、秩函数、有限差分等验证程序的终止性。最后,总结了各种验证方法的研究现状以及未来发展。The complete accuracy of the program include partial correctness and termination. In order to improve the correct- ness of program verification, the program, correcmess verification methods are introduced. The methods include those based on the complete accuracy of axiomatic verification procedures, based on the fixed point theorem, eigenvalue theory, rank function, finite difference and knowledge verification program termination. Finally, the various methods of current research and future development are summarized.

关 键 词：程序正确性 终止性 不动点 秩函数 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]