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 a program's total correctness, it is sufficient to prove its partial correctness, and its termination.[2] The latter kind of proof (termination proof) can never be fully automated, since the halting problem is undecidable."
Were correctness proof possible in general, it would already have been applied significantly in practice (and there would be no bugs 😀 ).
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
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: xml-dev-unsubscribe@lists.xml.org
subscribe: xml-dev-subscribe@lists.xml.org
List archive: http://lists.xml.org/archives/xml-dev/
List Guidelines: http://www.oasis-open.org/maillists/guidelines.php