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

A most interesting question. My thoughts tend in a direction different from pre- and post-conditions. The focus should be on the comparison of structured information. As you are speaking of "translation from one format to another", I consider information content as a possible yardstick. Imagine source and target formats can be mapped to their semantic information content - expressed e.g. by RDF or some other representation as recently presented at xmlprague 2024 [1]. The correctness of the transformation can then be assessed by comparing the information content of source and target. I think the possibility of mapping tree-structured information (XML, JSON, ...) to tree-independent information content does not receive the interest which it deserves.

Kind regards,

Hans-Jürgen

[1] Kottmann, Renzo; Cedric Pauken;  Andreas Schmitz: Simple Semantic Data Modeling in XML (SeMoX), xmlprague 2024

https://archive.xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf , p. 231 f

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?

For imperative languages, one way is to define a pre-condition which the

caller of a program or function must guarantee, and a post-condition

which describes what the program or function will achieve.  Written in a

Hoare triple, pre-condition P, post-condition Q, and code S can be

depicted as {P}S{Q}.

But the logical world illustrated by typical descriptions of Hoare

triples feels remarkably simple -- atomic values assigned to variables.

What language would one need in order to formulate plausible pre- and

post-conditions on XML transformations, or more generally on functions

or procedures that operate on XDM instances?

Asking for a friend.

--

C. M. Sperberg-McQueen

Black Mesa Technologies LLC

_______________________________________________________________________

XML-DEV is a publicly archived, unmoderated list hosted by OASIS

to support XML implementation and development. To minimize

spam in the archives, you must subscribe before posting.

[Un]Subscribe/change address: http://www.oasis-open.org/mlmanage/

Or unsubscribe: [email protected]

subscribe: [email protected]

List archive: http://lists.xml.org/archives/xml-dev/

List Guidelines: http://www.oasis-open.org/maillists/guidelines.php