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

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.


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