Cart
[Home] [By Thread] [By Date] [Recent Entries]
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
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] |
