An attack on a minty

>btw, I think with some of the Quick Check type systems you have the
>ability to over-ride the random number generator, so if you know of
>some good boundaries to check based on what is being checked, you can
>nudge things in that direction? for whatever it might/not be worth.

One insight I took away from QuickCheck is that if you have a rich type
system, you can use that to automatically guide generation of test cases.
You specify, for each type T, a way of generating a random instance
of T.  This does not need to come from the uniform distribution; the
distribution can be biased towards certain boundary cases.  For instance,
if T = int, the distribution might pick the numbers 0, 1, 2, -1, MAXINT,
MININT with probability 0.1 each and otherwise might pick a number
uniformly at random.  Moreover, if you have a recursive data type,
you can use this to generate random instances of recursive data types.
Then you can use the declared types on each function to guide generation
of test cases for that function.

Of course, you need a separate oracle to test for each input whether
the function behaved appropriately on that input.  This only gives you
testcase generation, not the oracle.

There's been some work on this kind of automatic testcase generation
for Java.  Take a look at Randoop:
  http://people.csail.mit.edu/cpacheco/randoop/0.1/doc/
Randoop has a default oracle (e.g., things like checking for unexpected
runtime exceptions from standard methods), but if you used runtime
assertion checking vigorously in your code, that might provide a better
oracle.  Also of interest may be JML's runtime assertion checker: you
can specify preconditions/postconditions/object invariants, and it will
insert runtime checks into your Java code to check whether these are
ever violated.

I wonder how useful this would be in other languages, such as the objcap
languages that we often discuss here.