Re: Testing relational databases

From: S Perryman <a_at_a.net>
Date: Tue, 11 Jul 2006 12:41:24 +0100
Message-ID: <e902p4$nd3$1_at_emma.aioe.org>


"Chris Smith" <cdsmith_at_twu.net> wrote in message news:MPG.1f1c35e83d04d493989776_at_news.altopia.net...

>S Perryman <a_at_a.net> wrote:

>> "Marshall" <marshall.spight_at_gmail.com> wrote ...

>>>S Perryman wrote:

SP>Design By Contract ??
SP> Specification-directed testing ??
SP> Design For Testability ??

SP>All techniques that by themselves or together will give you for a large SP> majority of systems exactly what "we want" .

>>> I don't follow. What are you trying to say?

>> The techniques (see above) to deliver what "we" want are already here.
>> :-)
>> And they work very well indeed.

> It's unclear what you mean by "design by contract",

The black-box definition of the behaviour of a component in terms of its operation pre/post/invariant conditions (similarly for the definition of the component implementation) .

> and specifically,
> whether you've got in mind tools that verify the contract universally or
> existentially.

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.

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

> Testing all possible computer states for a
> computer with even 1 MB of memory requires an amount of time that dwarfs
> the entire length of the universe to date.

I have an example of a tenpin bowling score calculator that I often use. The input space is O(10^19) , the output space is O(10^25) . Not something that can typically be exhaustively tested.

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.

Using design for testability, it is possible to derive a test infrastructure from the impl, that proves any impl is correct for any of the O(10^19) inputs, without explicitly stating which of the O(10^25) outputs is the correct result.

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

> I can tell you rather conclusively that static analysis tools perform
> some limited tasks rather well, but they are no where near proving
> correctness of arbitrary programs from arbitrary specs.

Companies such as Praxis are proving correctness for something. That "something" is things such as non-trivial safety-critical systems.

Regards,
Steven Perryman Received on Tue Jul 11 2006 - 13:41:24 CEST

Original text of this message