Re: [isabelle] Random term given its type



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




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