摘要
基于语法树的程序正确性验证方法是目前程序正确性验证全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性。该文在介绍基于语法树的程序正确性验证方法的基础上,借鉴无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出一种新的XML路径查询模型和树匹配算法,并展示了STM在程序正确性验证方面的前景。
The method of the proof of program correctness based on syntax trees is the fire - new research field. In this method, the program syntax trees is the checked object in proof procedure of program correctness, the property tree matching algorithm is adopted to proof the correctness target program.This article bases on the foundation of introduction of STM, uses the research result of unordered tree - inclusion matching, integrates the technology in software component query, proposes a new model of path query and tree matching algorithm, shows the prospect of STM in the last.
基金
省教育厅基金项目(KYH063103004)
关键词
程序正确性验证
树匹配
路径查询
匹配度
proof of program correctness
XML
tree matching path query
xpath matching degree
