Re: Testing relational databases
From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Mon, 10 Jul 2006 17:58:32 GMT
Message-ID: <czwsg.8751$pu3.196856_at_ursa-nb00s0.nbnet.nb.ca>
>>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.
Date: Mon, 10 Jul 2006 17:58:32 GMT
Message-ID: <czwsg.8751$pu3.196856_at_ursa-nb00s0.nbnet.nb.ca>
S Perryman wrote:
> "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" .
Tossing around a bunch of buzzwords with question marks does nothing to address P^N for large N. Received on Mon Jul 10 2006 - 19:58:32 CEST