基于PAR的树与图结构泛型算法通用验证和生成方法

Loop invariant plays a key role in the verification and generation of program.Since the Turing award winner Hoare proposed the grand challenge project of Verified Software, loop invariant has become the focus in academia again. Existing work could solve the construction of loop invariant for linear structures. As to non-linear data structures, the expression of loop invariant is very complex. The research selects tree and graph as objects, and then looks for a new strategy of developing loop invariant using recursive definition technique by in-depth studies of commonality of recursive problems with the structures of tree and graph. Further, it explores the verification and generation of generic algorithms for the structures of tree and graph. Finally, the project designs the implementation scheme for generic mechanisms in PAR platform. It will demonstrate that the recursive definition technique of loop invariant is feasible and effective for deriving and proving non-linear data structure generic algorithms.

循环不变式在程序生成和验证中起到不可缺少的关键作用。自从图灵奖获得者Hoare提出了Verified Software的宏伟计划后，循环不变式再次成为学术界的研究热点。已有工作对线性结构循环不变式的构造解决较好，但对于树与图结构，不变式的表达方式十分繁琐复杂，算法程序的生成及验证更加繁杂困难。本项目选取非线性结构中的树与图结构作为研究对象，通过进一步深入研究树、图递归问题的共性，利用递归定义思想，对树与图非递归算法循环不变式的新策略进行研究，基于PAR探索一套树与图上泛型算法的通用验证和生成方法，并在PAR平台C++程序生成系统中予以实现。本项研究对简化非线性结构泛型算法程序的推导和验证过程有重要意义，为特定领域算法开发的部分自动化奠定了基础。

本项目的研究重点为树与图等非线性数据结构。这些数据结构通常具有递归特征，因此在构建它们的非递归算法循环不变式时，采用传统方法会表示十分复杂，不仅难以理解，而且在算法程序的推导和证明上也具有一定的困难。因此，本项目选择非线性数据结构中的树与图结构作为研究对象，通过对树和图的递归问题的共性进一步研究，利用递归定义的思想，探究针对树和图的非递归算法循环不变式的新策略，并探讨一套树与图泛型算法的通用验证和生成方法。该方法已在PAR平台C++程序生成系统中实现。. 主要研究进展包括：.1.深入分析和比较基于现有循环不变式的开发技术，并提出不同类别算法的循环不变式开发技术，同时给出算法推导和验证策略。代表性研究成果共有6项。.2.研究非线性结构非递归算法循环不变式新策略。通过对大量树和图非递归算法循环不变式的研究，探索非线性结构非递归算法的循环不变式策略，并给出算法推导和验证方法。代表性研究成果共有3项。.3.形式化推导生成和验证树和图泛型算法程序。对树和图非递归算法进行形式化推导生成，并对具有共性特征的算法构造通用循环不变式生成泛型算法，最后验证泛型算法程序。代表性研究成果共有4项。.4.设计和实现PAR平台C++泛型程序生成系统。目标是通过Apla语言描述的泛型算法自动生成C++程序，PAR平台C++泛型程序生成系统被设计和实现。代表性研究成果共有6项。. 本项研究对于简化树和图问题的泛型算法程序的推导和验证具有重要意义，为某些特定领域的算法开发奠定了基础。在项目经费的支持下，该项目取得了预期的研究成果，共发表了17篇学术论文，包括12篇期刊论文和5篇会议论文，其中有1篇CCF-A论文。出版了1本学术专著，获得了1项实用新型专利，培养了5名硕士研究生毕业。