Re: Testing relational databases
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 ...
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 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