Re: [isabelle] Disproof methods with Word.thy and AutoCorres
Hi David and Scott,
So, in short, I think the problems are (at least?):
1. Many properties you might want to quickcheck appear to require
"lifted_globals" to be in the "enum" class, which it usually
2. The "ptr" type causes problems for "quickcheck" for reasons I don't
fully understand, which means that any property involving
a non-trivial "lifted_globals" will cause errors.
Is there anyone with quickcheck expertise that might be able to help
resolve these issues?
I do have some experience with quickcheck, but I do not know AutoCorres at all.
I nevertheless had a brief look at problem 1. At least for validity Hoare triples, the
enum requirement arises as follows:
AutoCorres defines validity of Hoare triples as follows:
"⦃P⦄ f ⦃Q⦄ ≡ ∀s. P s ⟶ (∀(r,s') ∈ fst (f s). Q r s')"
The unbounded universal quantifier over s causes the problem with the enum type class,
because the code equation for ∀ implements it by testing all values of the universe (which
it obtains from the enum type class). There are two ways to avoid the enum type class:
1. Make the quantifier bounded by P and generate the states from P. Then, P cannot be a
predicate of type "'s => bool" any more, so this is probably not viable. One could,
however, implement a pass in the preprocessor of the code generator that tries to rewrite
precondition instances into generators for states. Then, quickcheck would only test states
that actually satisfy the precondition, so quickcheck has a reasonable chance of finding
counterexamples. However, this only works if P can really be rewritten into a generator. I
expect that one would need generative versions of all the common functions that occur in
2. For quickcheck, it suffices to replace the quantifier by some generator for states
(rather than covering all states). To that end, you have to define a copy of the
quantifier and implement is with a code equation that tests the predicate in the points
generated by the generator and raises an exception (with Code.abort) after the generator
of states has been exhausted. This is probably less work in terms of setup than 1 and
works reliably, but it is unclear how good the generated states are. If hardly any of them
satisfy the precondition P, then test coverage is low.
If one wants to invest more work, one can also combine both approaches. If 1 fails, try 2.
I was not able to look at problem 2, because I have not found a small example where the
ptr causes an exception. If you provide one, I can have a look at this, too.
This archive was generated by a fusion of
Pipermail (Mailman edition) and