[XML-DEV Mailing List Archive Home] [By Thread] [By Date] [Recent Entries] [Reply To This Message]

Re: defining correctness for an XML transformation - how?

  • From: Hans-Juergen Rennau <hrennau@yahoo.de>
  • To: "xml-dev@lists.xml.org" <xml-dev@lists.xml.org>, "C. M. Sperberg-McQueen" <cmsmcq@b...>
  • Date: Wed, 3 Jul 2024 18:13:26 +0000 (UTC)

Re:  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


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

_______________________________________________________________________

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/



[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index]


PURCHASE STYLUS STUDIO ONLINE TODAY!

Purchasing Stylus Studio from our online shop is Easy, Secure and Value Priced!

Buy Stylus Studio Now

Download The World's Best XML IDE!

Accelerate XML development with our award-winning XML IDE - Download a free trial today!

Don't miss another message! Subscribe to this list today.
Email
First Name
Last Name
Company
Subscribe in XML format
RSS 2.0
Atom 0.3
 

Stylus Studio has published XML-DEV in RSS and ATOM formats, enabling users to easily subcribe to the list from their preferred news reader application.


Stylus Studio Sponsored Links are added links designed to provide related and additional information to the visitors of this website. they were not included by the author in the initial post. To view the content without the Sponsor Links please click here.

Site Map | Privacy Policy | Terms of Use | Trademarks
Free Stylus Studio XML Training:
W3C Member
Stylus Studio® and DataDirect XQuery ™are products from DataDirect Technologies, is a registered trademark of Progress Software Corporation, in the U.S. and other countries. © 2004-2013 All Rights Reserved.