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

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.

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

本项目以申请者早先提出的循环不变式定义为基础，展开相关理论研究，给出该定义的形式化表示，揭示新概念循环不变式的本质特征，建立其与逻辑算法、C++等可执行程序功能上的等价关系；进而在单变量赋值型程序循环不变式自动探测技术的基础上，研究多变量赋值型程序循环不变式自动探测的方法, 提出了多变量赋值型程序循环不变式自动探测的算法，构建新概念循环不变式自动探测系统实验原型；研究用Issible定理证明器验证自动探测系统所得循环不变式及其相关程序正确性的方法，建立了从程序规约与循环不变式的Radl表示到Issible表示的转换系统，实现高效可靠的验证。与美国Gries教授进行了友好的合作。项目完成过程中,沿着我们特有的技术路线占领了该领域的国际制高点, 特别是提出了多变量赋值型程序循环不变式自动探测的算法。这是循环不变式自动探测技术的重大突破，必将对软件的形式化开发和正确性证明产生巨大影响，达到了预定的研究目标。.本项目实施过程中，项目组已在IEEE TFS、IEEE TEC、IEEE TSC、IEEE TETC、IEEE TITS和理论性权威期刊ASC、COR等国际期刊和本领域一级（A类）国内学术期刊上发表论文26篇，其中SCI期刊发表论文8篇（SCI一区2篇，SCI二区1篇，SCI三区3篇，SCI四区2篇），EI论文8篇；国内一级学报论文2篇；会议论文10篇。标注19篇, 非标注7篇(本课题组成员是论文作者)