I mean that, like in the definition of `||`
True || _ = True
False || x = x
If you generalize this to `or`-ing a list of inputs, eg:
foldr (||) False list_of_bools
you can 'short-circuit' the test as soon as you find a 'True' value.
This is actually not the greatest example, since you can't actually
test it in finite number of tests, but you can test "half" the
function by testing a that lists like [True:undefined] or [False,
False, False, ... , True , undefined] return "True".
It's "short-circuiting" in the sense that it (like the `||` function)
doesn't need to see (necessarily) all of it's arguments to return a
correct result.
/Joe
On Oct 12, 2009, at 2:11 PM, Eugene Kirpichov wrote:
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 <jfred...@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 <ekirpic...@gmail.com>:
It is possible for functions with compact domain, not just finite.
2009/10/12 Joe Fredette <jfred...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
