[Haskell-cafe] is proof by testing possible?

Joe Fredette jfredett at gmail.com
Mon Oct 12 13:57:27 EDT 2009


Really? How? That sounds very interesting, I've got a fair knowledge  
of basic topology, I'd love to see an application
to programming...




On Oct 12, 2009, at 1:55 PM, Eugene Kirpichov wrote:

> It is possible for functions with compact domain, not just finite.
>
> 2009/10/12 Joe Fredette <jfredett at gmail.com>:
>> In general? No- If we had an implementation of the `sin` function,  
>> how can
>> testing a finite number of points along it determine
>> if that implementation is correct for every point?
>>
>> For specific functions (particularly those with finite domain), it is
>> possible. If you know the 'correct' output of every input, then  
>> testing each
>> input and ensuring correct output will work. Consider the  
>> definition of the
>> `not` function on booleans. The domain only has two elements (True  
>> and
>> False) and the range has only two outputs (True and False), so if I  
>> test
>> every input, and insure it maps appropriately to the specified  
>> output, we're
>> all set.
>>
>> Basically, if you can write your function as a big case statement  
>> that
>> covers the whole domain, and that domain is finite, then the  
>> function can be
>> tested to prove it's correctness.
>>
>> Now, I should think the Muad'Dib would know that, perhaps you  
>> should go back
>> to studying with the Mentats. :)
>>
>> /Joe
>>
>>
>>
>> On Oct 12, 2009, at 1:42 PM, muad wrote:
>>
>>>
>>> Is it possible to prove correctness of a functions by testing it?  
>>> I think
>>> the
>>> tests would have to be constructed by inspecting the shape of the  
>>> function
>>> definition.
>>>
>>> --
>>> View this message in context:
>>> http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html
>>> Sent from the Haskell - Haskell-Cafe mailing list archive at  
>>> Nabble.com.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
>
> -- 
> Eugene Kirpichov
> Web IR developer, market.yandex.ru



More information about the Haskell-Cafe mailing list