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

defining correctness for an XML transformation - how?

• From: "C. M. Sperberg-McQueen" <cmsmcq@blackmesatech.com>
• To: xml-dev@lists.xml.org
• Date: Wed, 03 Jul 2024 07:40:55 -0600

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

• Follow-Ups:
  • Re: defining correctness for an XML transformation - how?
    • From: Tony Graham <tgraham@antenna.co.jp>
  • Re: defining correctness for an XML transformation - how?
    • From: "Liam R. E. Quin" <liam@fromoldbooks.org>
  • Re: defining correctness for an XML transformation - how?
    • From: Dimitre Novatchev <dnovatchev@gmail.com>
  • Re: defining correctness for an XML transformation - how?
    • From: Hans-Juergen Rennau <hrennau@yahoo.de>