[Haskell-cafe] is proof by testing possible?

[Joe Fredette]

Oh- thanks for the example, I suppose you can disregard my other  
message.

I suppose this is a bit like short-circuiting. No?


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

> For example, it is possible to prove correctness of a function
> "negatedHead :: [Bool] -> Bool" by testing it on "True:undefined" and
> "False:undefined".
>
> 2009/10/12 Eugene Kirpichov <ekirpichov at gmail.com>:
>> 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
>>
>
>
>
> -- 
> Eugene Kirpichov
> Web IR developer, market.yandex.ru