新概念循环不变式及其自动探测技术研究

鉴于循环不变式在软件正确性证明中不可缺少的关键作用，自图灵奖得主Hoare 提出Verified Software的宏伟计划后，循环不变式的研究再次成为软件界的热点。本项目是即将结题的国基重大国际合作项目部分研究的继续和扩展。以申请者早先提出的循环不变式定义为基础，展开相关理论研究，给出该定义的形式化表示，揭示新概念循环不变式的本质特征，建立其与逻辑算法、C++等可执行程序功能上的等价关系；进而在单变量赋值型程序循环不变式自动探测技术的基础上，研究多变量赋值型程序循环不变式自动探测的方法和算法，构建新概念循环不变式自动探测系统；研究用Issible定理证明器验证自动探测系统所得循环不变式及其相关程序正确性的方法，建立从程序规约与循环不变式的Radl表示到Issible表示的转换系统，实现高效可靠的验证。加强与美国Gries教授的合作，沿着我们特有的技术路线尽快占领该领域的国际制高点。

The loop invariants take a core role in the design，proof and derivation of software, including components, services and algorithmic program．The research on loop invariant is the hot area once again since Hoare presented "verified software"grand challenge. Based on the definition presented by the applicant in early time, the related theory with the definition will be studied systematically, present form denotation of the definition, discover essence character of the new concept loop invariant, build the equivalent relation between function of logic algorithm, loop invariant and executable program like C++, etc.; study the method and algorithm of automatic detection for the programs of multivariable assignment statement based on the techniques of automatic detection of single assignment and build the system of automatic detection of the new concept loop invariant; study the approach of verifying the correctness of the loop invariant produced by the system of automatic detection and related program using Issible theorem verifier, build the transformation system from Radl specification to Issible language to make the verification correctness. We will make cooperation with Gries and to reach the highest scientific-peak of this research field along with our special research road.