Re: Testing relational databases

Chris Smith wrote:
> Marshall <marshall.spight_at_gmail.com> wrote:
> > 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.
>
> If you've got a proof that for all X, P(X), then that gets you
> everything you need.

If what you want to prove is some universally quantified simple property, then sure. And yes, this is the most common case. But sometimes you want to prove some existentially quantified property. Sometimes you want to prove something like

forall Invoices.CustomerId x
  exists Customers.CustomerId y
    x = y

This is a foreign key, and these are quite common. So I have to insist on the ability to write both universal and existential quantification.

> Assuming that the domain is non-empty, that also
> guarantees that there exists an X such that P(X).

Yes, and in such cases a witness is not much use.

> I don't understand why you say that you want a "witness".
> What good does the witness do after you've got a proof
> for all X (if, again, the domain of X is non-empty)?

Witnesses are useful with existential quantification. Which means they are also useful when producing the negation of a universal quantification. For example, say you want to assert forall x p(x), and the systems comes back and says "it is false." (Not: "I couldn't prove it" but "I proved the negation.") Now, in such cases, wouldn't you like a witness? In other words, the system supplies you with a proof of !forall x p(x), which is to say it proves exists x !p(x), and wouldn't you like to know at least one value of x for which !p(x). I sure would.

In fact, the familiar phrase, "tests cannot prove the absence of bugs; they can only prove the presence of them" is a direct consequence of the rules for negating quantified expressions. If your proof techinque only supports existential quantification, the only universal you can prove is in the negative.

> > 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.
>
> It seems to me that there are really two things going on here. Tests
> make lousy proofs.

As sympathetic to the sentiment as I am, I have to object to that phrase as insufficiently precise. A better way to say it would be "proofs of existentially quantified theorems make lousy proofs of universally quantified theorems" which I think is uncontroversial.

The best way IMHO to understand the limitations of testing is to understand the limits of the expressive power of existential quantification. Thus we again find ourselves in a position where having a formalism lead to better understanding.

> However, there are things that are hard to prove.
> The absence of typographical errors in a program, for example, is not
> amenable to sitting down and writing out a proof. As a deeper case,
> heuristics are often used for solving problems for which some means of
> formalizing a "correct" answer is not known. Often, the best one can do
> is to demonstrate that the heuristic seems to give fairly good results
> in a lot of common cases. Testing is fine for demonstrating this, and
> unit testing at least contains good regression testing.
>
> I am not a fan of the pervasive unit testing fad... but it's clearly not
> useless. Some testing is clearly required, if nothing else just to
> catch the typographical error case. A line needs to be drawn, though,
> somewhere between there and unit testing for the correctness of
> algorithms.

Marshall Received on Mon Jul 10 2006 - 19:02:30 CEST