智能CAA中基于语法树的程序正确性验证研究

A Study on Syntax Trees Based Program Correctness Validation in Intelligent CAA

基于语法树的程序正确性验证方法是目前程序正确性验证方面全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性.文章在介绍基于语法树的程序正确性验证方法的基础上,借鉴了无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出了一种新的XML路径查询模型和树匹配算法,在理论和方法上对这个方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法切实可行的解决方案.

The method of the validation of program correctness based on syntax trees is a fire-new research field. In this method, the program syntax trees are the checked objects in the validating procedure of program correctness, the appropriate tree matching algorithm is adopted to validate the correctness of the target program. Based on the introduction of STM for program correctness validation, we use the research result of unordered tree-inclusion matching, integrate the technology in software component query, and propose a new model of path query and tree matching algorithm. We also discuss basic problems in the implementation of this method in theory and algorithm. In addition, we present a solution to implement this method with XML.