Re: Testing relational databases

From: Chris Smith <>
Date: Tue, 11 Jul 2006 09:33:47 -0600
Message-ID: <>

S Perryman <> wrote:
> There are runtime environments (Eiffel etc) that will do the above.
> There are static analysis environments (SPARK, Larch etc) that will attempt
> to do the above.

So you mean either one. There are two cases, then. It's only the runtime testing that I entirely take exception to as being able to prove any universal statements about program correctness.

> > Certainly neither of the other techniques you listed are
> > sufficient to provide universal proofs of program behavior for computers
> > of any substantial size.
> A "universal" proof AFAIK is undecidable.

That's a cop-out, though. Undecidability is a good reason to be satisfied with a program that produces useful results in most practical cases but fails to make a decision in a few pathological cases. It is not a good reason to punt on the problem entirely. In practice, programs for which undecidability of behavior matters tend not to be correct, and it's okay for a static analysis tool to reject them.

> Using specification-directed testing, it is possible to derive an impl
> that only requires around 6000 test cases (as opposed to > 10^19) to show
> correctness.

No, it's not. It is possible to derive a testing scheme that only executes 6000 test cases, and chooses them well to minimize the probability of failure of the system after the tests pass. However, it remains possible that case #6001 would have failed. The paper I just found via Google on spec-directed testing is rather explicit about the fact that the technique only works if you assume some degree of rigorous development process such that bugs are intended to be rather trivial.

> So the techniques are out there.
> But certainly not with mainstream automated support.

We were talking about giving proofs of statements about program behavior under any set of circumstances. There certainly are tools for this, but they do not involve testing or runtime observation of any kind.

Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Received on Tue Jul 11 2006 - 17:33:47 CEST

Original text of this message