[Haskell-cafe] is proof by testing possible?

[Eugene Kirpichov]

What do you mean under short-circuiting here, and what is the connection?
The property that allows to deduce global correctness from correctness
on under-defined inputs is just continuity in the topological sense.

2009/10/12 Joe Fredette <jfredett at gmail.com>:
> 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
>
>



-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru