[XML-DEV Mailing List Archive Home] [By Thread] [By Date] [Recent Entries] [Reply To This Message]

Re: defining correctness for an XML transformation - how?

• From: "C. M. Sperberg-McQueen" <cmsmcq@blackmesatech.com>
• To: Dimitre Novatchev <dnovatchev@gmail.com>
• Date: Wed, 03 Jul 2024 18:55:36 -0600

Dimitre Novatchev <dnovatchev@gmail.com> writes:

> From Wikipedia:
>
> "In theoretical computer science, an algorithm is correct with respect
> to a 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]

Thank you; that suggests a direction of thought that might prove useful.

> ...
> 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.

Maybe, but I think:

- Even if proofs of correctness are not always (or even not usually)
  possible, they may be very useful in the cases where they are
  possible.

  Numbers are not, in general, computable: there are uncomputable
  numbers.  But computers to compute the subset of computable numbers
  for which we know how to write programs are still often thought
  useful.

- Even if proofs of correctness were in principle not possible for XML
  transformations (which I do not believe), there can be value in being
  able to define explicitly what conditions a particular program must
  meet in order to be correct.  From such a specification, test cases
  can be generated, and there are anecdotal reports that just writing
  down a formal statement of the pre- and post-conditions of a program
  is often helpful in avoiding errors.

  Which is part of the reason that my question focused not on how to
  prove a transformation correct, but how to specify what correctness is
  for that transform.

-- 
C. M. Sperberg-McQueen
Black Mesa Technologies LLC
http://blackmesatech.com

• References:
  • defining correctness for an XML transformation - how?
    • From: "C. M. Sperberg-McQueen" <cmsmcq@blackmesatech.com>
  • Re: defining correctness for an XML transformation - how?
    • From: Dimitre Novatchev <dnovatchev@gmail.com>