Re: defining correctness for an XML transformation - how?
Dimitre Novatchev <[email protected]> Wed, 3 Jul 2024 11:54:35 -0700
| Newsgroups | gmane.text.xml.devel |
|---|---|
| Message-ID | <CAK4KnZc=ke3g7qk1ZvXER=kNBHjGAO6fFE70WV4UNrCyCP4dSQ@mail.gmail.com> |
--000000000000593876061c5c5d85 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable From Wikipedia: "In theoretical computer science <https://en.wikipedia.org/wiki/Theoretical_computer_science>, an algorithm <https://en.wikipedia.org/wiki/Algorithm> is *correct* with respect to a specification <https://en.wikipedia.org/wiki/Program_specification> if it behaves as specified. Best explored is *functional* correctness, which refers to the input-output behavior of the algorithm: for each input it produces an output satisfying the specification.[1] <https://en.wikipedia.org/wiki/Correctness_(computer_science)#cite_note-fun= ctional-1> Within the latter notion, *partial correctness*, requiring that *if* an answer is returned it will be correct, is distinguished from *total correctness*, which additionally requires that an answer *is* eventually returned, i.e. the algorithm terminates. Correspondingly, to prove <https://en.wikipedia.org/wiki/Mathematical_proof> a program's total correctness, it is sufficient to prove its partial correctness, and its termination.[2] <https://en.wikipedia.org/wiki/Correctness_(computer_science)#cite_note-tot= alcorrectness-2> The latter kind of proof (termination proof <https://en.wikipedia.org/wiki/Termination_proof>) can never be fully automated, since the halting problem <https://en.wikipedia.org/wiki/Halting_problem> is undecidable <https://en.wikipedia.org/wiki/Undecidable_problem>." Were correctness proof possible in general, it would already have been applied significantly in practice (and there would be no bugs =F0=9F=98=80 = ). But what we have in reality is the* art *of software testing, with correctness testing being just one of its parts. When practicing TDD (Test Driven Development) correctness is defined by the available set of tests, and must be defined/constructed before any implementation is attempted. Then any implementation that passes all tests is considered "correct". Of course, the set of tests is constantly modified and generally extended over time and so the "proof of correctness" (running the set of tests) must be run successfully over and over again. And if the set of tests is constantly being modified, this means that there was no complete definition of the correctness at any time. It seems that this is the current state of the art (would love to be proven wrong!), and up to my knowledge there isn't a general way of proving that the initial or any current set of tests is solvable, due to, for example, such known factors as the halting problem. There might be a subset (or subsets) of the set of all problems, for which proof of correctness is possible, but I am not aware of such subsets having been defined, or, if defined, how useful is their scope. Anyway, there is no restriction on the sets of problems that one could attempt to solve with XSLT. And even if we could define "correctness", this would not be too useful if in general this "correctness" would not be possible to prove. Thanks, Dimitre On Wed, Jul 3, 2024 at 6:48=E2=80=AFAM C. M. Sperberg-McQueen < [email protected]> wrote: > 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 > > --=20 Cheers, Dimitre Novatchev --------------------------------------- Truly great madness cannot be achieved without significant intelligence. --------------------------------------- To invent, you need a good imagination and a pile of junk ------------------------------------- Never fight an inanimate object ------------------------------------- To avoid situations in which you might make mistakes may be the biggest mistake of all ------------------------------------ Quality means doing it right when no one is looking. ------------------------------------- You've achieved success in your field when you don't know whether what you're doing is work or play ------------------------------------- To achieve the impossible dream, try going to sleep. ------------------------------------- Facts do not cease to exist because they are ignored. ------------------------------------- Typing monkeys will write all Shakespeare's works in 200yrs.Will they write all patents, too? :) ------------------------------------- Sanity is madness put to good use. ------------------------------------- I finally figured out the only reason to be alive is to enjoy it. --000000000000593876061c5c5d85 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">From Wikipedia:<br><br>"In <a href=3D"https://en.wiki= pedia.org/wiki/Theoretical_computer_science" title=3D"Theoretical computer = science">theoretical computer science</a>, an <a href=3D"https://en.wikiped= ia.org/wiki/Algorithm" title=3D"Algorithm">algorithm</a> is <b>correct</b> = with respect to a <a href=3D"https://en.wikipedia.org/wiki/Program_specific= ation" class=3D"gmail-mw-redirect" title=3D"Program specification">specific= ation</a> if it behaves as specified. Best explored is <i>functional</i> correctness, which refers to the input-output behavior of the=20 algorithm: for each input it produces an output satisfying the=20 specification.<sup id=3D"gmail-cite_ref-functional_1-0" class=3D"gmail-refe= rence"><a href=3D"https://en.wikipedia.org/wiki/Correctness_(computer_scien= ce)#cite_note-functional-1">[1]</a></sup> <p>Within the latter notion, <i>partial correctness</i>, requiring that <i>= if</i> an answer is returned it will be correct, is distinguished from <i>t= otal correctness</i>, which additionally requires that an answer <i>is</i> = eventually returned, i.e. the algorithm terminates. Correspondingly, to <a = href=3D"https://en.wikipedia.org/wiki/Mathematical_proof" title=3D"Mathemat= ical proof">prove</a> a program's total correctness, it is sufficient t= o prove its partial correctness, and its termination.<sup id=3D"gmail-cite_= ref-totalcorrectness_2-0" class=3D"gmail-reference"><a href=3D"https://en.w= ikipedia.org/wiki/Correctness_(computer_science)#cite_note-totalcorrectness= -2">[2]</a></sup> The latter kind of proof (<a href=3D"https://en.wikipedi= a.org/wiki/Termination_proof" class=3D"gmail-mw-redirect" title=3D"Terminat= ion proof">termination proof</a>) can never be fully automated, since the <= a href=3D"https://en.wikipedia.org/wiki/Halting_problem" title=3D"Halting p= roblem">halting problem</a> is <a href=3D"https://en.wikipedia.org/wiki/Und= ecidable_problem" title=3D"Undecidable problem">undecidable</a>."<br><= br></p><p>Were correctness proof possible in general, it would already have= been applied significantly in practice (and there would be no bugs =F0=9F= =98=80 ).<br><br></p><p>But what we have in reality is the<b><i> art </i></= b>of software testing, with=C2=A0 correctness testing being just one of=20 its=20 parts.<br><br></p><p>When practicing TDD (Test Driven Development) correctn= ess is defined by the available set of tests, and must be defined/construct= ed before any implementation is attempted.</p><p>Then any implementation th= at passes all tests is considered "correct".</p><p>Of course, the= set of tests is constantly modified and generally extended over time and s= o the "proof of correctness" (running the set of tests) must be r= un successfully over and over again. And if the set of tests is constantly = being modified, this means that there was no complete definition of the cor= rectness at any time.<br><br></p><p>It seems that this is the current state= of the art (would love to be proven wrong!), and up to my knowledge there = isn't a general way of proving that the initial or any current set of t= ests is solvable, due to, for example, such known factors as the halting pr= oblem.<br><br></p><p>There might be a subset (or subsets) of the set of all= problems, for which proof of correctness is possible, but I am not aware o= f such subsets having been defined, or, if defined, how useful is their sco= pe.<br><br></p><p>Anyway, there is no restriction on the sets of problems t= hat one could attempt to solve with XSLT. And even if we could define "= ;correctness", this would not be too useful if in general this "c= orrectness" would not be possible to prove.<br><br></p><p>Thanks,<br><= /p><p>Dimitre<br></p></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" = class=3D"gmail_attr">On Wed, Jul 3, 2024 at 6:48=E2=80=AFAM C. M. Sperberg-= McQueen <<a href=3D"mailto:[email protected]">cmsmcq@blackmesatec= h.com</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"ma= rgin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:= 1ex">Roger Costello's recent question about how to show the correctness= of a<br> translation from one XML format to another very similar one suggests a<br> related question.=C2=A0 Forget *showing* that an XML transformation is<br> correct -- how would you define correctness formally, if you wanted to<br> be able in principle to provide a machine-checkable proof of<br> correctness?<br> <br> For imperative languages, one way is to define a pre-condition which the<br= > caller of a program or function must guarantee, and a post-condition<br> which describes what the program or function will achieve.=C2=A0 Written in= a<br> Hoare triple, pre-condition P, post-condition Q, and code S can be<br> depicted as {P}S{Q}.<br> <br> But the logical world illustrated by typical descriptions of Hoare<br> triples feels remarkably simple -- atomic values assigned to variables.<br> <br> What language would one need in order to formulate plausible pre- and<br> post-conditions on XML transformations, or more generally on functions<br> or procedures that operate on XDM instances?<br> <br> Asking for a friend.<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><br clear=3D"all"><br><span class=3D"gmail_signature_pre= fix">-- </span><br><div dir=3D"ltr" class=3D"gmail_signature"><div>Cheers,<= /div><div>Dimitre Novatchev</div><div>-------------------------------------= --</div><div>Truly great madness cannot be achieved without significant int= elligence.</div><div>---------------------------------------</div><div>To i= nvent, you need a good imagination and a pile of junk</div><div>-----------= --------------------------</div><div>Never fight an inanimate object</div><= div>-------------------------------------</div><div>To avoid situations in = which you might make mistakes may be the</div><div>biggest mistake of all</= div><div>------------------------------------</div><div>Quality means doing= it right when no one is looking.</div><div>-------------------------------= ------</div><div>You've achieved success in your field when you don'= ;t know whether what you're doing is work or play</div><div>-----------= --------------------------</div><div>To achieve the impossible dream, try g= oing to sleep.</div><div>-------------------------------------</div><div>Fa= cts do not cease to exist because they are ignored.</div><div>-------------= ------------------------</div><div>Typing monkeys will write all Shakespear= e's works in 200yrs.Will they write all patents, too? :)</div><div>----= ---------------------------------</div><div>Sanity is madness put to good u= se.</div><div>-------------------------------------</div><div>I finally fig= ured out the only reason to be alive is to enjoy it.</div><div>=C2=A0</div>= </div> --000000000000593876061c5c5d85--