A Simple and Efficient Step Towards Type-Correct XSLT Transformations

Abstract

XSLT 1.0 is a standardized functional  programming language and widely used for defining transformations on XML models and documents, in many areas of industry and publishing. The problem of XSLT type checking is to verify that a given transformation, when applied to an input which conforms to a given structure definition, e.g. an XML DTD, will always produce an output which adheres to a second structure definition. This problem is known to be  undecidable for the full range of XSLT and document structure definition languages. Either one or both of them must be significantly restricted, or only approximations can be calculated.
The algorithm presented here takes a different approach towards type
correct XSLT transformations. It does not consider the type of the input document at all. Instead it parses the fragments of the result document contained verbatim in the transformation code and   verifies that these can potentially appear in the result language,   as defined by a given DTD. This is a kind of abstract interpretation, which can be executed on the fly and in linear time when parsing the XSLT program. Generated error messages are located accurately to a child subsequence of a single result element node.
Apparently the method eliminates a considerable share of XSLT programming errors, on the same order of magnitude as a full fledged global control-flow analysis.