Re: Testing relational databases

"Marshall" <marshall.spight_at_gmail.com> wrote in message news:1152546436.639236.305120_at_75g2000cwc.googlegroups.com...

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

> http://en.wikipedia.org/wiki/SPARK_programming_language

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

Regards,
Steven Perryman Received on Mon Jul 10 2006 - 18:07:33 CEST