XML的逻辑
Logics for XML
摘要：
本文描述了XML处理语言的静态分析系统的理论和实践基础。该系统依赖于一个不动点的时间逻辑与逆，来自μ演算，其中模型是有限的树。这种演算的表现力足以捕捉规则的树类型以及树中的多向导航，同时具有单一的指数时间复杂度。具体地说，证明了该逻辑的可判定性在时间上为2^O（n），其中n是输入公式的大小。主要的XML概念被线性地转换为逻辑：XML导航和节点选择语义，以及常规树语言（包括DTD和XML模式）。基于这些嵌入，在XML应用程序中的几个主要重要的问题被减少到满足的逻辑。这些问题包括包含、空、等价、重叠、覆盖、存在或不存在常规树类型约束以及带注释查询的静态类型检查。然后重点是一个健全的和完整的算法来决定逻辑，以及详细的复杂性分析，和关键的实现技术，以建立一个有效的求解器。使用该系统的完整实现的实际实验。该系统似乎是有效的，在实践中的几个现实的情况。这项工作的主要应用是一个新的静态分析器类的程序设计语言使用的XML表达式和XML类型注释（输入和输出）。这样的分析器允许在编译时确保有价值的属性，如类型安全和优化，以实现更安全和更有效的XML处理。
英文摘要：
This thesis describes the theoretical and practical foundations of a system for the static analysis of XML processing languages. The system relies on a fixpoint temporal logic with converse, derived from the mu-calculus, where models are finite trees. This calculus is expressive enough to capture regular tree types along with multi-directional navigation in trees, while having a single exponential time complexity. Specifically the decidability of the logic is proved in time 2^O(n) where n is the size of the input formula. Major XML concepts are linearly translated into the logic: XPath navigation and node selection semantics, and regular tree languages (which include DTDs and XML Schemas). Based on these embeddings, several problems of major importance in XML applications are reduced to satisfiability of the logic. These problems include XPath containment, emptiness, equivalence, overlap, coverage, in the presence or absence of regular tree type constraints, and the static type-checking of an annotated query. The focus is then given to a sound and complete algorithm for deciding the logic, along with a detailed complexity analysis, and crucial implementation techniques for building an effective solver. Practical experiments using a full implementation of the system are presented. The system appears to be efficient in practice for several realistic scenarios. The main application of this work is a new class of static analyzers for programming languages using both XPath expressions and XML type annotations (input and output). Such analyzers allow to ensure at compile-time valuable properties such as type-safety and optimizations, for safer and more efficient XML processing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
