> > I guess what I would like is to reuse most of the mechanisms in
> > QuickCheck to have it say one of these two things:
> >
> > 1. Found an satisfying instance after 73 tries: [gives instance]
> >
> > 2. After 100 tries, could not find a satisfying instance.
> >
> > Like failure,
Norman,
I guess what I would like is to reuse most of the mechanisms in
QuickCheck to have it say one of these two things:
1. Found an satisfying instance after 73 tries: [gives instance]
2. After 100 tries, could not find a satisfying instance.
Like failure, the first tells you something
On Sun, 19 Oct 2008 00:39:32 +0200, Norman Ramsey <[EMAIL PROTECTED]> wrote:
I guess what I would like is to reuse most of the mechanisms in
QuickCheck to have it say one of these two things:
1. Found an satisfying instance after 73 tries: [gives instance]
2. After 100 tries, could not fin
> The answer is that QuickCheck can't correctly constructively verify an
> existential condition without a constructive mechanism to generate the
> existential (i.e. the Skolem function mentioned before).
I agree but don't think it's relevant. QuickCheck can't verify a
universal either.
> If
> there are similar
> scenarios on which I've already given up in despair, such as
writing a
> generator for creating well-typed terms in a nontrivial language.
This is something I've also struggled with. I'm coming to the
conclusion that it'd really be useful for the "Gen" monad to be
par
The answer is that QuickCheck can't correctly constructively verify an
existential condition without a constructive mechanism to generate the
existential (i.e. the Skolem function mentioned before).
If you think about it from a plausible reasoning and constructive logic
sense, QuickCheck should no
> > But how do I use QuickCheck to check an existential?
>
> The "standard" method in QuickCheck is to be constructive, and
> actually implement the function that constructs for the value. So,
> instead of
>
> forAll x . exists y . P(x,y)
>
> you write
>
> forAll x . P(x, find_y(
Hi Norman,
> But how do I use QuickCheck to check an existential?
The "standard" method in QuickCheck is to be constructive, and
actually implement the function that constructs for the value. So,
instead of
forAll x . exists y . P(x,y)
you write
forAll x . P(x, find_y(x))
for a suitably i
I recently used QuickCheck to check on some calculations for image compression.
(I love exact rational arithmetic!) But I thought only to check for
inverse properties, and I realized afterward I had failed to check for
ranges. For example I should have checked that
boundedB block = -1 <= b &&
