Re: [isabelle] Quickcheck-Narrowing



Hi Peter,


On 18/02/14 18:00, Andreas Lochbihler wrote:
Regarding Native_Word, it is important to think about the generation strategy. The
narrowing engine calls the generators whenever it encounters an variable in a goal in
order to refine it. For datatypes, the generator returns a list of refined terms such as
the constructors of the datatype. The generator for ints, however, just returns the
numbers around 0. A first attempt for words could be to produce the first few values of
the word, but I would expect better results if it also generates larger word values. In
principle, one can consider a word as a list of bits of fixed length and have the
generator behave similarly to the one for list.
Here are a few more thoughts on this. Refinement works for datatypes, because the functions on them are defined by pattern-matching. That is, when a variable is refined to the list of possible constructors, evaluation can continue and might even report a definitive value without examining the data structure any further. Since Native_Word maps the word types to atomic types in the target language, and operations to built-in operations which are usually strict, we cannot exploit incremental refinements here, because we cannot symbolically represent such words. Therefore, it is probably best to just enumerate values, maybe in some clever way. Narrowing in Quickcheck adapts LazySmallCheck from Haskell (http://hackage.haskell.org/package/lazysmallcheck), so I had a look there. Its generators for the primitive Haskell types also just enumerates some values.

Andreas




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