Should exhaustiveness testing be on by default?
Neil Mitchell
ndmitchell at gmail.com
Thu May 21 12:14:23 EDT 2009
> OK. i'm just trying to get an intuition for the analysis.
Catch is defined by a small Haskell program. You can write a small
Haskell evaluation for a Core language. The idea is to write the
QuickCheck style property, then proceed using Haskell style proof
steps. The checker is recursive - it assigns a precondition to an
expression based on the precondition of subexpressions, therefore I
just induct upwards proving that each step is correct individually.
There wasn't an intention of trying to move partiality around, but
perhaps it has worked out that way.
> What is the nature of the preconditions generated?
A precondition is a proposition of pairs of (expression, constraint),
where an pair is satisfied if the expression satisfies the constraint.
I prove that given a couple of lemmas about the constraint language,
the analysis is correct. I then prove that 2 particular constraint
languages have these necessary lemmas.
As a side note, I'm pretty certain that the constraint languages I
give aren't the best choice. The second one (MP constraints) is good,
but lacks an obvious normal form, which makes the fixed point stuff a
little more fragile/slow. I'm sure someone could come up with
something better, and providing it meets a few simple lemmas, it's
suitable for Catch.
> In order for them to
> cancel out the calls to error, are they constructed from information in
> the caller (as I speculated) about how the function under analysis is used?
Yes, information from case branches add to the constraint, so:
case xs of
[] -> []
_:_ -> head xs
becomes:
xs == [] \/ safe (head xs)
xs == [] \/ xs == _:_
True
> Obviously, you're also using a restricted notion of "bottom".
For my purposes, bottom = call to error. Things such as missing case
branches and asserts are translated to error. I actually consider
non-termination to be a safe outcome, for example Catch says:
assert (last xs) True
This is safe if all elements of the list are True (Catch approximates
here), or if the list xs is infinite.
Thanks
Neil
More information about the Glasgow-haskell-users
mailing list