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

Yes and no, I think. First, API integration is a huge topic and a major part of it is really the translation of information itself - not enhancement; second, if the ambition is limited to a partial validation, a contribution to validation, then you can regard any results concerning the semantic alignment as valuable pieces of information to be assembled. It is somewhat like logical chemistry: A is mapped to its semantic content A', B is mapped to B', then A' and B' are poured into one pot and we can measure what happens. An important aspect is the independence of the A to A' and B to B' mappings, as they are usable in combination with any C, D, ... for which a corresponding alignment has been defined.

Am Mittwoch, 3. Juli 2024 um 20:22:03 MESZ hat Michael Kay <mike@saxonica.com> Folgendes geschrieben:

>The correctness of the transformation can then be assessed by comparing the information content of source and target.

Only for transformations that aren't designed to remove any information or add any information. Those must surely be in a minority.

Michael Kay

Saxonica

On 3 Jul 2024, at 19:13, Hans-Juergen Rennau <hrennau@yahoo.de> wrote:

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

Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M. Sperberg-McQueen <cmsmcq@blackmesatech.com> Folgendes geschrieben:

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
http://blackmesatech.com

_______________________________________________________________________

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: xml-dev-unsubscribe@lists.xml.org
subscribe: xml-dev-subscribe@lists.xml.org
List archive: http://lists.xml.org/archives/xml-dev/
List Guidelines: http://www.oasis-open.org/maillists/guidelines.php