Re: Testing relational databases
Date: 10 Jul 2006 08:47:16 -0700
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.
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.
Marshall Received on Mon Jul 10 2006 - 17:47:16 CEST