Re: Testing relational databases

Bob Badour wrote:
>
> They are real math proofs.

For sure!

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

What we get with unit tests is existential quantification with programmer generated witnesses at compile time, so it's actually a start in the direction of what we want.

Of course, we run in to problems if we begin to claim that we can use existential quantification to demonstrate universal quantification; this is of course unsound. (In general.)

Marshall Received on Mon Jul 10 2006 - 17:47:16 CEST