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 - 12:58:32 CDT
