Re: defining correctness for an XML transformation - how?
Rick Jelliffe <[email protected]> Fri, 5 Jul 2024 16:42:59 +1000
| Newsgroups | gmane.text.xml.devel |
|---|---|
| Message-ID | <CADUdYQWHLfABWv-Zxo=Q_33iEk2LXiPxTBH+DNXdJY3sOuGGBg@mail.gmail.com> |
--0000000000008d16b7061c7a6017 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I haven't read all the thread so apologies if I am re-making some point, or saying something dumb that has been pointed out. Three quick points. 1. If your schema is recursive, then the problem of determining whether it is always correct is NP, isn't it? Infinite number of inputs. Which, if so, probably needs to limit or condition our expectations or approaches. 2. Obviously people use Schematron to validate pre and post conditions, including co-constraints between input and output all the time. it is a common use. (Where Schematron is lacking is that it does not have a built in mechanism to force completeness: obviously it can report if there are unexplained elements that no rule in a pattern catches, but it cannot enforce eg if there is an element found that is caught by no pattern... though you can make another pattern for that. ) What becomes useful (unless every element name is only used once per document instance) is for the transformation to generate some tracing data; so that e.g. for each output element we know which element ID or xpath of the input document(s) generated it. That gets rid of many logical errors: the issue is rarely "does this input value appear in the output" but rather "does this input value appear in the output because it actually came from that input?" 3. The problem might be considered as a category error: we do not actually want to validate the Inputs and outputs, we want to validate the XSLT. I came up with an approach for a bank years ago where I converted an XSLT into just the possible element branches it could generate. This then could be stitched in with other similar data from subsequent stages in the pipeline, so that the result was an abstract document (on a spreadsheet) that showed for each input what elements could appear in the final output. This helped them feel on top of the pipeline, to reason about flaws and behaviour, without needing XSLT expertise. This then could be paired with data extracted from a schema: for example to just do pairwise tests: for every parent/child in the abstract output, is it an allowed pair by the output schema? (IIRC James Clark put in a partial validation mode in Jing that allowed you to just test parent-child constraints not sequence or absense: this could be useful too. ) Are any required pairs missing in the input or output? Rick On Fri, Jul 5, 2024 at 3:01=E2=80=AFAM C. M. Sperberg-McQueen < [email protected]> wrote: > > Roger L Costello <[email protected]> writes: > > > Michael Sperberg-McQueen made this fascinating statement: > > > > ... my question [is] focused not on how to prove a transformation > > correct, but how to specify what correctness is for that > > transform. > > > > I would really like to understand that. What is the difference between > > =E2=80=9Cproving a transformation is correct=E2=80=9D versus =E2=80=9Cs= pecifying what > > correctness is for a transform=E2=80=9D? > > (Michael Kay has already answered this pretty well; this is partly to > say that I agree with what he said and partly to add a simple example.) > > The second is (the formulation of) a statement; the first is (the > construction of) a proof that the statement is true. > > For example: Suppose we specify as follows the correctness of a > transformation T taking input I and producing output O: > > pre-condition: I is an XML document containing zero or more > Airport_Name elements. > > post-condition: O is an XML document containing zero or more 'name' > elements, such that > > (1) for every Airport_Name element $i in I, there is some name > element $o in O such that $o has only one child node (a text > node) and string($o) =3D normalize-space($i); > > (2) for every name element $o in O, there is some Airport_Name > element $i in I such that string($o) =3D normalize-space($i). > > Then for any specific input/output pair we can imagine checking that the > pre-condition and post-condition both hold. If I have succeeded in > making the specification unambiguous, it should always be clear whether > a given pair of I and O do or do not satisfy the conditions. From this > spec, for example, it's clear that any name in the input may occur any > non-zero number of times in the output, and any name in the output may > have occurred any non-zero number of times in the input, and that the > ordering of names in the output, and the structure of the output > document, are not constrained. > > And to prove T correct, instead of just proving an individual I/O pair > correct, we can imagine proving that *whenever* the pre-condition is > satisfied, the result of running T will *always* satisfy the > post-condition. Suppose T is written in XSLT. Then we might want to > show that for every Airport_Name element in I, a particular template > will be evaluated, that that template produces zero or more suitable > 'name' elements, and that no other template in the stylesheet will > produce any 'name' elements. Or we might show that a particular > variable is assigned a sequence of strings containing every distinct > Airport_Name string in I, and that a given expression in the stylesheet > serializes them all in 'name' elements (and again that nothing else in > the program will ever produce a 'name' element). > > [Note: the example pre- and post-conditions I've given are formulated in > English; many people prefer a more formal language, because > statements in more formal languages can be manipulated > mechanically in ways that are helpful. Proving that T satisfies > its specification can similarly be done in prose or in a purely > formal way. > > We get more confidence that the proof is correct if it can be > checked mechanically, but plenty of anecdotal evidence suggests > that even writing conditions and proofs in prose can reduce the > defect rate for software. (See for example the 'clean room > engineering' approach developed by Harlan Mills at IBM, perhaps > best described as 'semi-formal'.) There are also anecdotal > reports that just formulating the pre- and post-conditions helps, > even if there is no effort to produce a proof. I find this > plausible, since formulating pre- and post-conditions even in > prose makes me think about the program and possible edge cases in > a way that I do not otherwise always do. > > I will be happiest if the answer to my question of the other day > describes a formal language analogous to those used in formal > proofs of correctness for imperative languages, but suitable for > XML. Even a coherent account of how to formulate clear, crisp, > complete, and accurate specifications of correctness in prose, > however, would look to me like progress. End of note.] > > I hope this helps. > > Michael > > -- > 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 > > --0000000000008d16b7061c7a6017 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">I haven't read all the thread=C2=A0 so apologies if I = am re-making some point, or saying something dumb that has been pointed out= .<div dir=3D"auto"><br></div><div dir=3D"auto">Three quick points.</div><di= v dir=3D"auto"><br></div><div dir=3D"auto">1. If your schema is recursive, then the problem of determining whether it is always correct is NP, isn't it? Infinite number of inputs. Which, i= f so, probably needs to limit or condition our expectations or=20 approaches.</div><div dir=3D"auto"><br></div><div dir=3D"auto">2. Obviously= =20 people use Schematron to validate pre and post conditions, including=20 co-constraints between input and output all the time. it is a common=20 use.=C2=A0</div><div dir=3D"auto"><br></div><div dir=3D"auto">(Where Schema= tron=20 is lacking is that it does not have a built in mechanism to force=20 completeness: obviously it can report if there are unexplained elements=20 that no rule in a pattern catches, but it cannot enforce eg if there is=20 an element found that is caught by no pattern... though you can make=20 another pattern for that. )</div><div dir=3D"auto"><br></div><div dir=3D"au= to">What becomes useful (unless every element name is only used once per document i= nstance) is for the=20 transformation=C2=A0 to generate some tracing data; so that e.g. for=20 each output element we know which element ID or xpath of the input document= (s) generated it. That gets rid of many logical errors: the issue is rarely "does this input= =20 value appear in the output" but rather "does this input value app= ear in=20 the output because it actually came from that input?"=C2=A0</div><div = dir=3D"auto"><br></div><div dir=3D"auto">3. The problem might be considered as a category error: we do not actually want to validate the Inputs and outputs, we want to validate the XSLT. I came up with an approach for a bank years ago where I converted an XSLT into just the possible element branches it could generate. This then=20 could be stitched in with other similar data from subsequent stages in=20 the pipeline, so that the result was an abstract document (on a=20 spreadsheet) that showed for each input what elements could appear in=20 the final output.=C2=A0 This helped them feel on top of the pipeline, to=20 reason about flaws and behaviour, without needing XSLT expertise.</div><div= dir=3D"auto"><br></div><div dir=3D"auto">This then could be paired with data extracted from a schema: for example to=20 just do pairwise tests: for every parent/child in the abstract output,=20 is it an allowed pair by the output schema? (IIRC James Clark put in a=20 partial validation mode in Jing that allowed you to just test=20 parent-child constraints not sequence or absense: this could be useful=20 too. )=C2=A0 Are any required pairs missing in the input or output?</div><f= ont color=3D"#888888"><div dir=3D"auto"><br></div><div dir=3D"auto">Rick</d= iv><div dir=3D"auto"><br><br></div></font></div><br><div class=3D"gmail_quo= te"><div dir=3D"ltr" class=3D"gmail_attr">On Fri, Jul 5, 2024 at 3:01=E2=80= =AFAM C. M. Sperberg-McQueen <<a href=3D"mailto:[email protected]= ">[email protected]</a>> wrote:<br></div><blockquote class=3D"gma= il_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,2= 04,204);padding-left:1ex"><br> Roger L Costello <<a href=3D"mailto:[email protected]" target=3D"_blank= ">[email protected]</a>> writes:<br> <br> > Michael Sperberg-McQueen made this fascinating statement:<br> ><br> >=C2=A0 =C2=A0 =C2=A0... my question [is] focused not on how to prove a = transformation<br> >=C2=A0 =C2=A0 =C2=A0correct, but how to specify what correctness is for= that<br> >=C2=A0 =C2=A0 =C2=A0transform.<br> ><br> > I would really like to understand that. What is the difference between= <br> > =E2=80=9Cproving a transformation is correct=E2=80=9D versus =E2=80=9C= specifying what<br> > correctness is for a transform=E2=80=9D?<br> <br> (Michael Kay has already answered this pretty well; this is partly to<br> say that I agree with what he said and partly to add a simple example.)<br> <br> The second is (the formulation of) a statement; the first is (the<br> construction of) a proof that the statement is true.<br> <br> For example: Suppose we specify as follows the correctness of a<br> transformation T taking input I and producing output O:<br> <br> =C2=A0 =C2=A0pre-condition:=C2=A0 I is an XML document containing zero or m= ore<br> =C2=A0 =C2=A0Airport_Name elements.<br> <br> =C2=A0 =C2=A0post-condition: O is an XML document containing zero or more &= #39;name'<br> =C2=A0 =C2=A0elements, such that<br> <br> =C2=A0 =C2=A0 =C2=A0(1) for every Airport_Name element $i in I, there is so= me name<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0element $o in O such that $o has only one= child node (a text<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0node) and string($o) =3D normalize-space(= $i);<br> <br> =C2=A0 =C2=A0 =C2=A0(2) for every name element $o in O, there is some Airpo= rt_Name<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0element $i in I such that string($o) =3D = normalize-space($i).<br> <br> Then for any specific input/output pair we can imagine checking that the<br= > pre-condition and post-condition both hold.=C2=A0 If I have succeeded in<br= > making the specification unambiguous, it should always be clear whether<br> a given pair of I and O do or do not satisfy the conditions.=C2=A0 From thi= s<br> spec, for example, it's clear that any name in the input may occur any<= br> non-zero number of times in the output, and any name in the output may<br> have occurred any non-zero number of times in the input, and that the<br> ordering of names in the output, and the structure of the output<br> document, are not constrained.<br> <br> And to prove T correct, instead of just proving an individual I/O pair<br> correct, we can imagine proving that *whenever* the pre-condition is<br> satisfied, the result of running T will *always* satisfy the<br> post-condition.=C2=A0 Suppose T is written in XSLT.=C2=A0 Then we might wan= t to<br> show that for every Airport_Name element in I, a particular template<br> will be evaluated, that that template produces zero or more suitable<br> 'name' elements, and that no other template in the stylesheet will<= br> produce any 'name' elements.=C2=A0 Or we might show that a particul= ar<br> variable is assigned a sequence of strings containing every distinct<br> Airport_Name string in I, and that a given expression in the stylesheet<br> serializes them all in 'name' elements (and again that nothing else= in<br> the program will ever produce a 'name' element).<br> <br> [Note: the example pre- and post-conditions I've given are formulated i= n<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0English; many people prefer a more formal langua= ge, because<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0statements in more formal languages can be manip= ulated<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0mechanically in ways that are helpful.=C2=A0 Pro= ving that T satisfies<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0its specification can similarly be done in prose= or in a purely<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0formal way.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0We get more confidence that the proof is correct= if it can be<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0checked mechanically, but plenty of anecdotal ev= idence suggests<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0that even writing conditions and proofs in prose= can reduce the<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0defect rate for software.=C2=A0 (See for example= the 'clean room<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0engineering' approach developed by Harlan Mi= lls at IBM, perhaps<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0best described as 'semi-formal'.)=C2=A0 = There are also anecdotal<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0reports that just formulating the pre- and post-= conditions helps,<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0even if there is no effort to produce a proof.= =C2=A0 I find this<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0plausible, since formulating pre- and post-condi= tions even in<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0prose makes me think about the program and possi= ble edge cases in<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0a way that I do not otherwise always do.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0I will be happiest if the answer to my question = of the other day<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0describes a formal language analogous to those u= sed in formal<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0proofs of correctness for imperative languages, = but suitable for<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0XML.=C2=A0 Even a coherent account of how to for= mulate clear, crisp,<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0complete, and accurate specifications of correct= ness in prose,<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0however, would look to me like progress.=C2=A0 E= nd of note.]<br> <br> I hope this helps.<br> <br> Michael<br> <br> -- <br> C. M. Sperberg-McQueen<br> Black Mesa Technologies LLC<br> <a href=3D"http://blackmesatech.com" rel=3D"noreferrer" target=3D"_blank">h= ttp://blackmesatech.com</a><br> <br> _______________________________________________________________________<br> <br> XML-DEV is a publicly archived, unmoderated list hosted by OASIS<br> to support XML implementation and development. To minimize<br> spam in the archives, you must subscribe before posting.<br> <br> [Un]Subscribe/change address: <a href=3D"http://www.oasis-open.org/mlmanage= /" rel=3D"noreferrer" target=3D"_blank">http://www.oasis-open.org/mlmanage/= </a><br> Or unsubscribe: <a href=3D"mailto:[email protected]" target= =3D"_blank">[email protected]</a><br> subscribe: <a href=3D"mailto:[email protected]" target=3D"_bl= ank">[email protected]</a><br> List archive: <a href=3D"http://lists.xml.org/archives/xml-dev/" rel=3D"nor= eferrer" target=3D"_blank">http://lists.xml.org/archives/xml-dev/</a><br> List Guidelines: <a href=3D"http://www.oasis-open.org/maillists/guidelines.= php" rel=3D"noreferrer" target=3D"_blank">http://www.oasis-open.org/maillis= ts/guidelines.php</a><br> <br> </blockquote></div> --0000000000008d16b7061c7a6017--