Re: [xml-dev] defining correctness for an XML transformation - how?

[Tony Graham <tgraham@antenna.co.jp>]

On 03/07/2024 14:40, C. M. Sperberg-McQueen wrote:
> Roger Costello's recent question about how to show the correctness of
> a translation from one XML format to another very similar one
> suggests a related question.  Forget *showing* that an XML
> transformation is correct -- how would you define correctness
> formally, if you wanted to be able in principle to provide a
> machine-checkable proof of correctness?
If it was 2007 and you were using DTDs and XSLT 1.0, you could try the
XML graph method from 'Static validation of XSL transformations':

   https://dl.acm.org/doi/10.1145/1255450.1255454

---

XSL Transformations (XSLT) is a programming language for defining
transformations among XML languages. The structure of these languages is
formally described by schemas, for example using DTD or XML Schema,
which allows individual documents to be validated. However, existing
XSLT tools offer no static guarantees that, under the assumption that
the input is valid relative to the input schema, the output of the
transformation is valid relative to the output schema.

We present a validation technique for XSLT based on the XML graph
formalism introduced in the static analysis of JWIG Web services and
XACT XML transformations. Being able to provide static guarantees, we
can detect a large class of errors in an XSLT stylesheet at the time it
is written instead of later when it has been deployed, and thereby
provide benefits similar to those of static type checkers for modern
programming languages.

Our analysis takes a pragmatic approach that focuses its precision on
the essential language features but still handles the entire XSLT
language. We evaluate the analysis precision on a range of real
stylesheets and demonstrate how it may be useful in practice.

---

Regards,


Tony Graham.
--
Senior Architect
XML Division
Antenna House, Inc.
----
Skerries, Ireland
tgraham@antenna.co.jp