Re: defining correctness for an XML transformation - how?
Hans-Juergen Rennau <[email protected]> Wed, 3 Jul 2024 18:13:26 +0000 (UTC)
| Newsgroups | gmane.text.xml.devel |
|---|---|
| Message-ID | <[email protected]> |
------=_Part_1509866_852303086.1720030406689
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
A most interesting question. My thoughts tend in a direction different fro=
m pre- and post-conditions. The focus should be on the comparison of struct=
ured information. As you are speaking of "translation from one format to an=
other", I consider information content as a possible yardstick. Imagine sou=
rce 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 as=
sessed by comparing the information content of source and target. I think t=
he possibility of mapping tree-structured information (XML, JSON, ...) to t=
ree-independent information content does not receive the interest which it =
deserves.
Kind regards,Hans-J=C3=BCrgen
[1] Kottmann,=C2=A0Renzo; Cedric Pauken;=C2=A0 Andreas=C2=A0Schmitz:=C2=A0S=
imple Semantic Data Modeling in XML (SeMoX), xmlprague 2024https://archive.=
xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf=C2=A0, p. 231 f
Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M. Sperberg-McQueen <=
[email protected]> Folgendes geschrieben: =20
=20
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.=C2=A0 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.=C2=A0 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.
--=20
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
=20
------=_Part_1509866_852303086.1720030406689
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
<html><head></head><body><div class=3D"ydp36b3e5cayahoo-style-wrap" style=
=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px=
;"><div></div>
<div dir=3D"ltr" data-setdir=3D"false"><div><div dir=3D"ltr" style=
=3D"font-family: Helvetica Neue, Helvetica, Arial, sans-serif;">A most inte=
resting question. My thoughts tend in a direction different from pre- and p=
ost-conditions. The focus should be on the comparison of structured informa=
tion. As you are speaking of "translation from one format to another", I co=
nsider information content as a possible yardstick. Imagine source and targ=
et 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 co=
mparing the information content of source and target. I think the possibili=
ty of mapping tree-structured information (XML, JSON, ...) to tree-independ=
ent information content does not receive the interest which it deserves.</d=
iv><div dir=3D"ltr" style=3D"font-family: Helvetica Neue, Helvetica, Arial,=
sans-serif;"><br clear=3D"none"></div><div dir=3D"ltr" style=3D"font-famil=
y: Helvetica Neue, Helvetica, Arial, sans-serif;">Kind regards,</div><div d=
ir=3D"ltr" style=3D"font-family: Helvetica Neue, Helvetica, Arial, sans-ser=
if;">Hans-J=C3=BCrgen</div><div dir=3D"ltr" style=3D"font-family: Helvetica=
Neue, Helvetica, Arial, sans-serif;"><br clear=3D"none"></div><div dir=3D"=
ltr" style=3D"font-family: Helvetica Neue, Helvetica, Arial, sans-serif;">[=
1] Kottmann, Renzo; Cedric Pauken; Andreas <span style=3D"c=
olor: rgb(0, 0, 0);">Schmitz: </span>Simple Semantic Data Modeling in =
XML (SeMoX), xmlprague 2024</div><div dir=3D"ltr" style=3D"font-family: Hel=
vetica Neue, Helvetica, Arial, sans-serif;"><a shape=3D"rect" href=3D"https=
://archive.xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf" style=3D=
"color: rgb(25, 106, 212); text-decoration-line: underline;" rel=3D"nofollo=
w" target=3D"_blank">https://archive.xmlprague.cz/2024/files/xmlprague-2024=
-proceedings.pdf</a> , p. 231 f</div></div><br></div><div><br></div>
=20
</div><div id=3D"ydp173f1a58yahoo_quoted_0923868499" class=3D"ydp17=
3f1a58yahoo_quoted">
<div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
=20
<div>
Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M=
. Sperberg-McQueen <[email protected]> Folgendes geschrieben:
</div>
<div><br></div>
<div><br></div>
=20
=20
<div><div dir=3D"ltr">Roger Costello's recent question abou=
t how to show the correctness of a<br></div><div dir=3D"ltr">translation fr=
om one XML format to another very similar one suggests a<br></div><div dir=
=3D"ltr">related question. Forget *showing* that an XML transformatio=
n is<br></div><div dir=3D"ltr">correct -- how would you define correctness =
formally, if you wanted to<br></div><div dir=3D"ltr">be able in principle t=
o provide a machine-checkable proof of<br></div><div dir=3D"ltr">correctnes=
s?<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr">For imperative lang=
uages, one way is to define a pre-condition which the<br></div><div dir=3D"=
ltr">caller of a program or function must guarantee, and a post-condition<b=
r></div><div dir=3D"ltr">which describes what the program or function will =
achieve. Written in a<br></div><div dir=3D"ltr">Hoare triple, pre-con=
dition P, post-condition Q, and code S can be<br></div><div dir=3D"ltr">dep=
icted as {P}S{Q}.<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr">But =
the logical world illustrated by typical descriptions of Hoare<br></div><di=
v dir=3D"ltr">triples feels remarkably simple -- atomic values assigned to =
variables.<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr">What langua=
ge would one need in order to formulate plausible pre- and<br></div><div di=
r=3D"ltr">post-conditions on XML transformations, or more generally on func=
tions<br></div><div dir=3D"ltr">or procedures that operate on XDM instances=
?<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr">Asking for a friend.=
<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr">-- <br></div><div dir=
=3D"ltr">C. M. Sperberg-McQueen<br></div><div dir=3D"ltr">Black Mesa Techno=
logies LLC<br></div><div dir=3D"ltr"><a href=3D"http://blackmesatech.com" r=
el=3D"nofollow" target=3D"_blank">http://blackmesatech.com</a><br></div><di=
v dir=3D"ltr"><br></div><div dir=3D"ltr">__________________________________=
_____________________________________<br></div><div dir=3D"ltr"><br></div><=
div dir=3D"ltr">XML-DEV is a publicly archived, unmoderated list hosted by =
OASIS<br></div><div dir=3D"ltr">to support XML implementation and developme=
nt. To minimize<br></div><div dir=3D"ltr">spam in the archives, you must su=
bscribe before posting.<br></div><div dir=3D"ltr"><br></div><div dir=3D"ltr=
">[Un]Subscribe/change address: <a href=3D"http://www.oasis-open.org/mlmana=
ge/" rel=3D"nofollow" target=3D"_blank">http://www.oasis-open.org/mlmanage/=
</a><br></div><div dir=3D"ltr">Or unsubscribe: <a href=3D"mailto:xml-dev-un=
[email protected]" rel=3D"nofollow" target=3D"_blank">xml-dev-unsubsc=
[email protected]</a><br></div><div dir=3D"ltr">subscribe: <a href=3D"mail=
to:[email protected]" rel=3D"nofollow" target=3D"_blank">xml-=
[email protected]</a><br></div><div dir=3D"ltr">List archive: <a =
href=3D"http://lists.xml.org/archives/xml-dev/" rel=3D"nofollow" target=3D"=
_blank">http://lists.xml.org/archives/xml-dev/</a><br></div><div dir=3D"ltr=
">List Guidelines: <a href=3D"http://www.oasis-open.org/maillists/guideline=
s.php" rel=3D"nofollow" target=3D"_blank">http://www.oasis-open.org/maillis=
ts/guidelines.php</a><br></div><div dir=3D"ltr"><br></div></div>
</div>
</div></body></html>
------=_Part_1509866_852303086.1720030406689--