Francois Lachance wrote:

> Con,  Any XSLT transform will halt. Try writing an XSLT transform that
> nests elements that we provoke an infinite loop. It breaks.
> The processor
> returns an error. That counts as halting.  The XSLT file is
> validated by
> the processor.

Hi Francois

While it's true that some xslt processors will detect infinite loops, it is in principle not possible to detect all such loops. The XSLT spec itself warns about this issue, pointing out that running 3rd-party stylesheets may present a denial-of-service threat.

http://www.zvon.org/xxl/XSLTreference/W3C/xslt.html#section-Applying-Template-Rules

Some XSLT processors may give up after recursing a certain number of times, but this is implementation-specific, and not in conformance with the spec. NB a stylesheet can recurse without producing output, so detecting an overflow of the output buffer is also not a 100% reliable way to detect a non-terminating transform.

Anyway ... my point was really that automated proof of XSLT transforms (even of the halting problem, let alone compliance of the output to a particular schema) is not only infeasible, but actually theoretically impossible _in the general case_.

That said, I do think it's a feasible (and valuable) project to attempt to prove "output-document-schema-compliance" of stylesheets which are constrained in various ways (e.g. to refer only to the "child" or "descendant" axes in apply-templates; not calling named-templates at all, or at least, not recursively).

Cheers

Con