Simple and Effective Relation-Based Approaches To XPath and XSLT Type Checking (Technical Report, Bad Honnef 2015)

TL;DR

This paper introduces relation-based methods for type checking in XPath and XSLT, providing concise semantics and practical analysis tools for XML document transformations and addressing key challenges in type validation.

Contribution

It presents a novel relation-based approach for XPath and XSLT type checking, enabling practical and concise validation techniques for XML transformations.

Findings

Relational interpretation simplifies XPath semantics.

Practical analysis tool for XPath 1.0 node-set fragment.

Fragmented validation technique for XSLT transformations.

Abstract

XPath is a language for addressing parts of an XML document. We give an abstract interpretation of XPath expressions in terms of relations on document node types. Node-set-related XPath language constructs are mapped straightforwardly onto basic, well-understood and easily computable relational operations. Hence our interpretation gives both extremely concise type-level denotational semantics and a practical analysis tool for the node-set fragment of the XPath 1.0 language. This method is part of the TPath implementation of XPath. XSL-T is a pure functional language for transforming XML documents. For the most common case, the transformation into an XML document, type checking of the transformation code is unfeasible in general, but strongly required in practice. It turned out that the relational approach of TPath can be carried over to check all fragments of the result language, which are contained verbatim in the transformation code. This leads to a technique called "Fragmented Validation" and is part of the txsl implementation of XSL-T.