Re: defining correctness for an XML transformation - how?
Michael Kay <[email protected]> Wed, 3 Jul 2024 19:21:52 +0100
| Newsgroups | gmane.text.xml.devel |
|---|---|
| Message-ID | <[email protected]> |
--Apple-Mail=_39CC4110-60B3-4FAC-9C37-52BD84F3B824 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 >The correctness of the transformation can then be assessed by comparing = the information content of source and target.=20 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 <[email protected]> wrote: >=20 > 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. >=20 > Kind regards, > Hans-J=C3=BCrgen >=20 > [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 >=20 >=20 > 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. 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? >=20 > 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}. >=20 > But the logical world illustrated by typical descriptions of Hoare > triples feels remarkably simple -- atomic values assigned to = variables. >=20 > 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? >=20 > Asking for a friend. >=20 > -- > C. M. Sperberg-McQueen > Black Mesa Technologies LLC > http://blackmesatech.com <http://blackmesatech.com/> >=20 > = _______________________________________________________________________ >=20 > 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. >=20 > [Un]Subscribe/change address: http://www.oasis-open.org/mlmanage/ > Or unsubscribe: [email protected] = <mailto:[email protected]> > subscribe: [email protected] = <mailto:[email protected]> > List archive: http://lists.xml.org/archives/xml-dev/ > List Guidelines: http://www.oasis-open.org/maillists/guidelines.php >=20 --Apple-Mail=_39CC4110-60B3-4FAC-9C37-52BD84F3B824 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 <html><head><meta http-equiv=3D"content-type" content=3D"text/html; = charset=3Dutf-8"></head><body style=3D"overflow-wrap: break-word; = -webkit-nbsp-mode: space; line-break: after-white-space;">><span = style=3D"font-family: "Helvetica Neue", Helvetica, Arial, = sans-serif;">The correctness of the transformation can then be assessed = by comparing the information content of source and = target. </span><div><font face=3D"Helvetica Neue, Helvetica, Arial, = sans-serif"><br></font></div><div><font face=3D"Helvetica Neue, = Helvetica, Arial, sans-serif">Only for transformations that aren't = designed to remove any information or add any information. Those must = surely be in a minority.</font></div><div><font face=3D"Helvetica Neue, = Helvetica, Arial, sans-serif"><br></font></div><div><font = face=3D"Helvetica Neue, Helvetica, Arial, sans-serif">Michael = Kay</font></div><div><font face=3D"Helvetica Neue, Helvetica, Arial, = sans-serif">Saxonica<br = id=3D"lineBreakAtBeginningOfMessage"></font><div><br><blockquote = type=3D"cite"><div>On 3 Jul 2024, at 19:13, Hans-Juergen Rennau = <[email protected]> wrote:</div><br = class=3D"Apple-interchange-newline"><div><div><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 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.</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;">Kind regards,</div><div dir=3D"ltr" style=3D"font-family: = Helvetica Neue, Helvetica, Arial, sans-serif;">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"">Schmitz: </span>Simple Semantic Data Modeling in XML = (SeMoX), xmlprague 2024</div><div dir=3D"ltr" style=3D"font-family: = Helvetica 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"nofollow" = target=3D"_blank">https://archive.xmlprague.cz/2024/files/xmlprague-2024-p= roceedings.pdf</a> , p. 231 f</div></div><br></div><div><br></div> =20 </div><div id=3D"ydp173f1a58yahoo_quoted_0923868499" = class=3D"ydp173f1a58yahoo_quoted"> <div style=3D"font-family:'Helvetica Neue', Helvetica, = Arial, sans-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 = about how to show the correctness of a<br></div><div = dir=3D"ltr">translation from one XML format to another very similar one = suggests a<br></div><div dir=3D"ltr">related question. Forget = *showing* that an XML transformation 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 to provide a = machine-checkable proof of<br></div><div = dir=3D"ltr">correctness?<br></div><div dir=3D"ltr"><br></div><div = dir=3D"ltr">For imperative languages, 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<br></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-condition P, post-condition Q, and code S can be<br></div><div = dir=3D"ltr">depicted 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><div 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 language would one need in = order to formulate plausible pre- and<br></div><div = dir=3D"ltr">post-conditions on XML transformations, or more generally on = functions<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 Technologies LLC<br></div><div dir=3D"ltr"><a = href=3D"http://blackmesatech.com/" rel=3D"nofollow" = target=3D"_blank">http://blackmesatech.com</a><br></div><div = 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 development. To = minimize<br></div><div dir=3D"ltr">spam in the archives, you must = subscribe 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/mlmanage/" 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:[email protected]" rel=3D"nofollow" = target=3D"_blank">[email protected]</a><br></div><div = dir=3D"ltr">subscribe: <a href=3D"mailto:[email protected]" = rel=3D"nofollow" = target=3D"_blank">[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/guidelines.php" = rel=3D"nofollow" = target=3D"_blank">http://www.oasis-open.org/maillists/guidelines.php</a><b= r></div><div dir=3D"ltr"><br></div></div> </div> </div></div></div></blockquote></div><br></div></body></html>= --Apple-Mail=_39CC4110-60B3-4FAC-9C37-52BD84F3B824--