Specification and Verification for Semi-Structured Data

作     者：CHEN Tao-lue HAN Ting-ting LU Jian 

作者机构：State Key Laboratory of Novel Software TechnologyNanjing University Nanjing 210093 Jiangsu China 

出 版 物：《Wuhan University Journal of Natural Sciences》 (武汉大学学报（自然科学英文版）)

年 卷 期：2006年第11卷第1期

页      面：107-112页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Supported by the National Natural Sciences Foun-dation of China (60233010  60273034  60403014)  863 ProgramofChina (2002AA116010)  973 Programof China (2002CB312002) 

主　　题：semi structured data tree logic fixpoint model checking algorithm 

摘      要：Tree logic, inherited from ambient logic, is introduced as the formal foundation of related programming language and type systems, In this paper, we introduce recursion into such logic system, which can describe the tree data more dearly and concisely. By making a distinction between proposition and predicate, a concise semantics interpretation for our modal logic is given. We also develop a model checking algorithm for the logic without △ operator. The correctness of the algorithm is shown. Such work can be seen as the basis of the semi-structured data processing language and more flexible type system.