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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users