Re: Testing relational databases

Marshall <marshall.spight_at_gmail.com> wrote:
> 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.

I am going to have to object here. Existential quantifications inside of universal quantifications are just as useless for testing as anything else. I'm not referring to the "forall Invoices.CustomerId x" which is actually rather inconsequential, but rather to the implied universal quantification that is always there: (I'm going to abuse your notation here. Please look away if you have a weak stomach, and cover the eyes of any nearby small children.)

forall possible program states and inputs   forall Invoices.CustomerId x
    exists Customers.CustomerId y
      x = y

Even if what I want to prove is "there is a customer with ID 0", what I really mean is:

forall possible program states and inputs   exists Customers.CustomerId x
    x = 0

So there's still a universal quanitification on the outside. Testing is not only unsufficient to prove the universal quantifications that you say out loud; it's also insufficient to prove that implied "for all possible program states and inputs" there.

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

Yes, I would! If the program is incorrect, it's certainly nice to know why. I was simply commenting on the set of circumstances in which the program can be reasonably considered correct.

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

You're right, of course. I mean "tests make lousy proofs of program correctness".

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

Sure, so long as you understand that program correctness is not an existential quality (okay, except when there is only one set of input to the program).

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation