¿Qué es una reducción, con respecto a QuickCheck de Haskell?
Cuando QuickCheck encuentra una entrada que viola una propiedad, primero tratará de encontrar entradas más pequeñas que también violen la propiedad, para darle al desarrollador un mejor mensaje sobre la naturaleza de la falla.
Lo que significa ser "pequeño" por supuesto depende del tipo de datos en cuestión; para QuickCheck es cualquier cosa que sale de la función de shrink
.
Se explica mejor en una sesión QuickCheck:
Prelude Test.QuickCheck> let prop l = all (/= 5) l Prelude Test.QuickCheck> quickCheck prop *** Failed! Falsifiable (after 10 tests and 2 shrinks): [5]
Así que aquí QuickCheck fue capaz de dar el contra-ejemplo más pequeño, pero a juzgar por los comentarios, primero tenía una lista más grande en mente y luego la reducía usando shrink
. Para ver más de cerca lo que está sucediendo, usamos verboseCheck
:
Prelude Test.QuickCheck> verboseCheck prop Passed: [] Passed: [0] Passed: [-2,1] Passed: [-2,2,-2] Passed: [-4] Failed: [-1,-2,5,4,2] *** Failed! Passed: [] Failed: [5,4,2] Passed: [] Passed: [4,2] Failed: [5,2] Passed: [] Passed: [2] Failed: [5] Passed: [] Passed: [0] Passed: [3] Passed: [4] Falsifiable (after 6 tests and 3 shrinks): [5]
QuickCheck prueba algunas listas para las cuales se sostiene la proposición, y luego encuentra [-1,-2,5,4,2]
. Ahora reduce la lista, intentando sublistas de la misma. Puede convencerse a sí mismo en GHCi que shrink [-1,-2,5,4,2] == [[],[5,4,2],[-1,-2,2],...
y el la segunda entrada es la primera que aún falla la prueba. QuickCheck continúa con eso y se contrae aún más: shrink [5,4,2] == [[],[4,2],[5,2],...
, y shrink [5,2] [[],[2],[5],...
aún más shrink [5,2] [[],[2],[5],...
Por último, intenta contraerse [5]
más, pero ninguno de shrink [5] == [[],[0],[3],[4]]
falla la proposición, por lo que el ejemplo de recuento final es [5]
.
Un solo shrink
es una reducción gradual de la complejidad de algún caso de prueba Arbitrary
(un "encogimiento inmediato"). Esto podría ser algo así como 2 -> 1
o 1:[] -> []
. Para tipos más complejos, puede haber varias formas de "encoger incrementalmente" un tipo para que los especifique a todos en una lista.
Por ejemplo, los árboles pueden encogerse al eliminar una sola hoja, por lo tanto, si hay n
hojas, el encogimiento produce una lista de longitud n
.