Should exhaustiveness testing be on by default?
Don Stewart
dons at galois.com
Thu May 21 12:17:36 EDT 2009
ndmitchell:
> > 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, that's helpful, and much what I expected.
-- Don
More information about the Glasgow-haskell-users
mailing list