Re: Testing relational databases

From: Bob Badour <>
Date: Mon, 10 Jul 2006 17:58:32 GMT
Message-ID: <czwsg.8751$>

S Perryman wrote:

> "Marshall" <> wrote in message 

>>Bob Badour wrote:

>>>If you think Ada has anything to do with writing sound software,

>>A small point of clarification: the item being discussed was SPARK,
>>which as I understand it is a static analysis tool for a subset of ADA.
>>In fact they actually do proof of properties of their code. I have
>>little information about it, but the approach at least is interesting.


>>>A proof has a good chance of approaching 100% certainty and a
>>>much better chance than a unit test does.

>>It is an interesting thing about unit tests: they actually are a
>>kind of proof. Specifically, a unit test is a existentially quantified
>>proof of a particular property, via a programmer-generated
>>witness to that property.
>>For example, let us say we wished to consider commutativity
>>of addition. We could write a test:
>>test1() { assertEquals(3+5, 5+3); }
>>We can interpret this as a proof and a witness. The theorem is
>>exists x, y: x+y = y+x
>>and the proof is that the test passes. Further we have the
>>witness (x=3, y=5).

>>Now, I would argue that what we most often want is actually
>>not existential quantification but universal quantification. In fact,
>>what we *really* want is existential quantification, universal
>>quantification, and witnesses, and we want them all available
>>both at compile time and at runtime. And we want the
>>witnesses to be system generated wherever possible.
> Design By Contract ??
> Specification-directed testing ??
> Design For Testability ??
> All techniques that by themselves or together will give you for a large
> majority of systems exactly what "we want" .

Tossing around a bunch of buzzwords with question marks does nothing to address P^N for large N. Received on Mon Jul 10 2006 - 19:58:32 CEST

Original text of this message