Cart
[Home] [By Thread] [By Date] [Recent Entries]
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. Kind regards, Hans-Jürgen [1] Kottmann, Renzo; Cedric Pauken; Andreas Schmitz: Simple Semantic Data Modeling in XML (SeMoX), xmlprague 2024
Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M. Sperberg-McQueen <cmsmcq@b...> Folgendes geschrieben:
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 _______________________________________________________________________ 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: xml-dev-unsubscribe@l... subscribe: xml-dev-subscribe@l... List archive: http://lists.xml.org/archives/xml-dev/ List Guidelines: http://www.oasis-open.org/maillists/guidelines.php
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] |
