defining correctness for an XML transformation - how?

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