¿Cómo puedo probar una función de orden superior con QuickCheck?

Question

Tengo una función de orden superior que quiero probar, y una de las propiedades que quiero probar es qué hace con las funciones que se pasan. A modo de ejemplo, aquí hay un ejemplo artificial:

gen :: a -> ([a] -> [a]) -> ([a] -> Bool) -> a 

La idea es más o menos que se trata de un generador de ejemplo. Comenzaré con un solo a, crearé una lista simple de [a], luego haré nuevas listas de [a] hasta que un predicado me diga que pare. Una llamada podría tener este aspecto:

gen init next stop 

donde

init :: a 
next :: [a] -> [a] 
stop :: [a] -> Bool 

Aquí es la propiedad que desea probar:

En cualquier llamada a gen init next stop, gen promesas que nunca pasan de una lista vacía al next.

¿Puedo probar el inmueble con QuickCheck, y si es así, ¿cómo?

Answer 1

Mientras que sería útil que le dio la implementación de gen, soy adivinando que es algo como esto:

gen :: a -> ([a] -> [a]) -> ([a] -> Bool) -> a 
gen init next stop = loop [init] 
    where 
    loop xs | stop xs = head xs 
      | otherwise = loop (next xs) 

La propiedad que desea probar es que next Nunca se suministra un lista vacía . Un obstáculo para probar esto es que desea verificar un invariante de bucle interno dentro de gen, por lo que debe estar disponible en en el exterior. Vamos a modificar gen para devolver esta información:

genWitness :: a -> ([a] -> [a]) -> ([a] -> Bool) -> (a,[[a]]) 
genWitness init next stop = loop [init] 
    where 
    loop xs | stop xs = (head xs,[xs]) 
      | otherwise = second (xs:) (loop (next xs)) 

Utilizamos second de Control.Arrow. El original gen es fácil de definir en términos de genWitness:

gen' :: a -> ([a] -> [a]) -> ([a] -> Bool) -> a 
gen' init next stop = fst (genWitness init next stop) 

Gracias a la evaluación perezosa esto no nos va a dar mucho de arriba. Volver a la propiedad! Para permitir que se muestren las funciones generadas desde QuickCheck, usamos el módulo Test.QuickCheck.Function. Si bien no es estrictamente necesario aquí, una buena costumbre es monomorfizar la propiedad: utilizamos listas de Int s en lugar de permitir la restricción de monomorfismo convirtiéndolos en listas de unidades. Vamos ahora a afirmar la propiedad:

prop_gen :: Int -> (Fun [Int] [Int]) -> (Fun [Int] Bool) -> Bool 
prop_gen init (Fun _ next) (Fun _ stop) = 
    let trace = snd (genWitness init next stop) 
    in all (not . null) trace 

Vamos a tratar la ejecutarlo con QuickCheck:

ghci> quickCheck prop_gen 

algo parece bucle ... Sí, por supuesto: si gen bucles stop en las listas desde next nunca es True!Veamos en lugar de tratar de mirar prefijos finitas del rastreo de entrada lugar:

prop_gen_prefix :: Int -> (Fun [Int] [Int]) -> (Fun [Int] Bool) -> Int -> Bool 
prop_gen_prefix init (Fun _ next) (Fun _ stop) prefix_length = 
    let trace = snd (genWitness init next stop) 
    in all (not . null) (take prefix_length trace) 

Ahora obtenemos rápidamente aa contraejemplo:

385 
{_->[]} 
{_->False} 
2 

La segunda función es el argumento next, y si devuelve la lista vacía, , luego el bucle en gen dará next una lista vacía.

Espero que esto responda a esta pregunta y que le dé alguna información en cómo probar las funciones de orden superior con QuickCheck.

Answer 2

Es posiblemente de mal gusto abusar de esto, pero QuickCheck hace que falle una función si arroja una excepción. Entonces, para probar, simplemente dele una función que arroje una excepción para el caso vacío. La adaptación de la respuesta de danr:

import Test.QuickCheck 
import Test.QuickCheck.Function 
import Control.DeepSeq 

prop_gen :: Int -> (Fun [Int] [Int]) -> (Fun [Int] Bool) -> Bool 
prop_gen x (Fun _ next) (Fun _ stop) = gen x next' stop `deepseq` True 
    where next' [] = undefined 
     next' xs = next xs 

Esta técnica no requiere que modifique gen.