Email Gateway (Aug 22 2022 at 14:52): Email Gateway (Aug 22 2022 at 14:52):From: Omar Montano Rivas <omarmrivas@gmail.com>
Hi,
Is there a function in Isabelle/ML to generate a random term of a given a
type (and potentially instantiate type vars).
e.g.
val random_term : int -> typ -> term
where the first parameter is a seed and the second is the type of the
random term.
If not, would be difficult to use existing Quickcheck or Nitpick code to
program such function?
I was looking at the files src/HOL/Tools/Quickcheck/random_generators.ML
and exhaustive_generators.ML but I could not figure out how to use the ML
structures.
Thanks,
Email Gateway (Aug 22 2022 at 14:52):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi Omar,
a few years ago, a student at the Isabelle chair in Munich wrote a
bachelor thesis, which created a property-based testing tool (based on
previous quickcheck for ML implementation). Unfortunately, I could not
found a public available link to this bachelor thesis. The source code
is however available in the directory src/Tools/Spec_Check.
Especially, the function to create a random term was implemented in
http://isabelle.in.tum.de/repos/isabelle/file/628b271c5b8b/src/Tools/Spec_Check/generator.ML#l222.
Personally, I would also suggest to experiment with an alternative
generator that exhaustively enumerates small terms.
The randomly generated terms at larger size might have a very low
probability to fulfil the conditions you are interested in. Hence,
checking all small terms might be more successful; an observation that
has led us to choose exhaustive testing for the auto quickcheck tool
in Isabelle.
Lukas
Last updated: Apr 20 2024 at 08:16 UTC