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
      can't be.

   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 preconditions.

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.

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.