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 <[email protected]>: > 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 <[email protected]>: >>> >>> It is possible for functions with compact domain, not just finite. >>> >>> 2009/10/12 Joe Fredette <[email protected]>: >>>> >>>> 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 >>>>> [email protected] >>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>>> >>>> _______________________________________________ >>>> Haskell-Cafe mailing list >>>> [email protected] >>>> 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
