¿Cómo obtengo buenas (pequeñas) contracciones de QuickCheck?

Question

Estoy intentando ejecutar QuickCheck en algunas listas anidadas, algo que se parece a esto:

type Constraint = Text 
data Value = Value [Constraint] 
data Literal = Literal Value [Value] 
type Formula = [Literal] 

Así que una fórmula es una lista de literales, cada una de las cuales contiene un predicado y algunos argumentos; predicado/argumentos son valores que son una disyunción de restricciones en forma de cadena cada uno. Eso nos da una lista de listas de listas, ¡uf!

Si una de mis propiedades de QuickCheck falla, tiendo a obtener una cantidad incomprensible de resultados. Antes de experimentar con Shrink, solía sortear esto teniendo instancias arbitrarias que solo podían generar un pequeño conjunto de valores (pequeños). Implementar la función de reducción para cada uno de mis tipos parece ayudar un poco, pero no tanto como me gustaría. Todavía tengo una página llena de resultados.

Creo que lo que quiero de shrink es una pequeña lista de literales, donde cada literal tiene una pequeña lista de valores, que a su vez tiene pocas restricciones, cada una de las cuales es lo más corta posible. Pero en mis esfuerzos actuales, al menos estas listas son lo suficientemente grandes como para que la producción sea horrible. Si trato de ajustar mis implementaciones de reducción, también descubro que el control de calidad comienza a tomar mucho tiempo (¿en busca de psiquiatras?), Lo que amortigua mis esfuerzos por reducir el tamaño efectivamente.

¿Cómo mejora sus posibilidades de comprender las fallas de QuickCheck cuando ha anidado datos como este?

Answer 1

Tuve un problema similar, pero estaba usando C y el generador de ejemplo hecho en casa :) Tuve una implementación lenta y correcta, y rápida e incorrecta.

Utilizando ejemplos aleatorios, cuando encuentre un ejemplo incorrecto, le sugiero que disminuya el ejemplo. (Esto, por supuesto, podría o debería hacerse por programa, en lugar de por computadora)

Si tiene un predicado para esta prueba, y tiene un ejemplo que no funciona, intente eliminar elementos de listas de todas las órdenes (Esto debería ser un orden lineal de magnitud de llamadas) y para cada intento si falla la prueba.

Si sigue fallando, no hay razón para mantener esto en el ejemplo.

Si comienza a pasar, entonces este elemento debe permanecer en un ejemplo reducido.

(Esto es codicioso y no es óptima, pero sí ejecutar en el poli, en lugar de tiempo exponencial, y funcionó para mí)

Para mirada más científica, que sugieren el capítulo "La simplificación de los problemas" del libro "WHY PROGRAMS FAIL: A Guide to Systematic Debugging" por A.Zeller.

Nota: esto es sobre todo lo que hace contracción ...

Answer 2

Fwiw, echar un vistazo a https://github.com/leepike/SmartCheck, que pretende obtener mejores psiquiatras que uno normalmente puede hacer manualmente.