Propriedades e testes com QuickCheck
Propriedades em vez de exemplos, geradores automáticos e leitura de contraexemplos.
Um teste de exemplo verifica reverse [1,2,3] == [3,2,1]. Uma propriedade afirma algo sobre uma família de entradas: reverse (reverse xs) == xs para listas finitas.
O QuickCheck gera casos e procura um que viole a afirmação. Os testes observam esses casos; a afirmação universal continua a exigir uma demonstração.
A primeira propriedade
Propriedades são funções que devolvem Bool, com tipos concretos para a ferramenta saber o que gerar:
import Test.QuickCheck
prop_revRev :: [Int] -> Bool
prop_revRev xs = reverse (reverse xs) == xsNo GHCi, com o pacote QuickCheck instalado:
ghci> quickCheck prop_revRev
+++ OK, passed 100 tests.A ferramenta gerou 100 listas aleatórias1, que podem incluir listas vazias, comprimentos distintos, negativos e repetidos. A igualdade valeu em todas.
Um teste de exemplo verifica a entrada escolhida. A propriedade permite testar outras entradas automaticamente, mas só os casos gerados foram observados.
Contrato da ordenação
Uma função de ordenação deve produzir uma lista ordenada com os mesmos elementos e multiplicidades. Em [2,1,2], devolver [1,2] conserva os valores distintos, mas perde uma ocorrência. Devolver [2,1,2] conserva tudo, mas não ordena.
A idempotência f (f xs) == f xs verifica outra lei. A função f xs = [] satisfaz essa igualdade para qualquer lista finita, embora perca os dados. Para caracterizar a ordenação, testa a ordem e a conservação das multiplicidades. Quando tens uma implementação de referência independente, podes comparar os resultados.
Quando falha: o contraexemplo
Uma propriedade falsa dá um contraexemplo reduzido. Afirma que ordenar é a identidade:
import Data.List (sort)
prop_sortId :: [Int] -> Bool
prop_sortId xs = sort xs == xsghci> quickCheck prop_sortId
*** Failed! Falsifiable (after 3 tests):
[1,0]O QuickCheck responde que a propriedade é falsificável e mostra a testemunha [1,0]; o shrinking tenta reduzir a entrada encontrada conservando a falha, embora as reduções disponíveis não garantam o mínimo global. O número de testes varia de corrida para corrida, mas a lista curta fora de ordem é o essencial. Perante uma falha, compara o contraexemplo com o contrato antes de mudar a implementação; neste caso, a ordenação está certa e a propriedade é que está errada:
A propriedade idempotente da ordenação passa:
prop_sortSort :: [Int] -> Bool
prop_sortSort xs = sort (sort xs) == sort xsghci> quickCheck prop_sortSort
+++ OK, passed 100 tests.Geradores e condições
Por omissão, o QuickCheck gera valores arbitrários do tipo pedido: a distribuição e os limites dependem da instância Arbitrary e do parâmetro de tamanho. Quando a propriedade só faz sentido sob uma condição, impõe-na com ==>:
prop_divMod :: Integer -> Integer -> Property
prop_divMod x y = y /= 0 ==> (x `div` y) * y + (x `mod` y) == xOs casos com y == 0 são descartados e não contam como testes bem-sucedidos. Se a pré-condição for rara, a ferramenta pode desistir sem obter a amostra pedida. Um gerador que constrói entradas válidas evita gastar a maior parte das tentativas em descartes.
Um gerador à medida é uma ação que produz valores com a forma que queres. Para testar que o máximo de um par ordenado é o segundo elemento, gera pares já ordenados:
parOrdenado :: Gen (Int, Int)
parOrdenado = do
x <- arbitrary
y <- arbitrary
return (min x y, max x y)
prop_maxDireita :: Property
prop_maxDireita = forAll parOrdenado $ \(x, y) -> max x y == yGeramos dois inteiros e colocamos o menor primeiro, por isso todas as tentativas produzem um par válido que o forAll usa para testar a propriedade. suchThat é outra possibilidade, mas repete tentativas até satisfazer a condição, e uma condição impossível ou muito rara pode impedir a geração de terminar.
forAll não reduz automaticamente entradas de um gerador próprio; usa forAllShrink com um redutor que preserve a condição quando precisares desse comportamento.
O mesmo princípio aplica-se a insert x xs: se o contrato pressupõe xs ordenada, ordena a lista gerada antes de testar a inserção, para cada tentativa exercitar uma entrada válida.
Um contraexemplo que cabe no papel
A lei reverse (xs ++ ys) == reverse xs ++ reverse ys é falsa. Com xs=[1] e ys=[2], o lado esquerdo é [2,1] e o direito [1,2]. A lei correta troca a ordem das partes: reverse (xs ++ ys) == reverse ys ++ reverse xs. Este exemplo distingue a ordem de concatenação sem depender de acaso ou de um grande conjunto de dados.
Para justificar uma propriedade, identifica ainda o domínio. A igualdade envolvendo length pressupõe listas finitas; leis aritméticas em Int podem ser afetadas por overflow. Usar Integer numa propriedade de aritmética exata evita confundir uma falha matemática com o limite da representação.
Notas de rodapé
-
Os 100 casos são a omissão da ferramenta; podes pedir mais com argumentos de configuração. Voltar
Exercícios
Trocar a ordem das partes
Qual lei vale para listas finitas?
Pista
Usa listas com um elemento distinto em cada parte.
Solução
A ordem correta é reverse ys antes de reverse xs.
reverse (xs++ys) == reverse ys ++ reverse xs. Inverter a concatenação troca a ordem das partes.reverse (xs++ys) == reverse xs ++ reverse ys. Falha com xs=[1],ys=[2].reverse xs == xs. Só vale para listas que coincidem com a sua inversão.
Erros frequentes
Não uses listas iguais nos dois argumentos, que escondem a troca.
Uma propriedade insuficiente
Por que f(f xs)=f xs não prova que f ordena corretamente?
Pista
Experimenta uma função constante.
Solução
f xs=[] é idempotente mas perde os dados. Uma ordenação
deve produzir uma lista ordenada com as mesmas ocorrências da entrada.
Confere a tua resposta:
- Dou uma função errada que satisfaz a lei.
- Exijo conservação de elementos e multiplicidades.
- Exijo ordem do resultado.
Erros frequentes
Testar uma lei verdadeira não significa que ela caracterize todo o contrato.
Testar uma ordenação contra implementações erradas
Escreve prop_ordena :: ([Int] -> [Int]) -> Property. Gera listas com valores entre -10 e 10, incluindo a possibilidade de lista vazia. A propriedade deve exigir saída ordenada e os mesmos elementos com as mesmas multiplicidades.
Mostra um contraexemplo para f xs = [] e outro para f xs = xs. Compara com sort. Se o gerador for usado com forAll, há redução automática dos contraexemplos?
Pista
Solução
Podemos comparar multiplicidades com uma referência independente e comparar vizinhos para a ordem:
import Data.List (sort)
import Test.QuickCheck
ordenada :: [Int] -> Bool
ordenada xs = and (zipWith (<=) xs (drop 1 xs))
prop_ordena :: ([Int] -> [Int]) -> Property
prop_ordena f = forAll genLista $ \xs ->
let ys = f xs
in ordenada ys && sort ys == sort xs
where
genLista :: Gen [Int]
genLista = listOf (choose (-10,10))sort ys == sort xs compara todas as ocorrências, incluindo valores fora do intervalo que uma implementação errada pudesse inventar. A função constante falha para [0]: [] perde esse elemento. A identidade falha para [1,0]: conserva os dados, mas a saída não está ordenada. sort satisfaz ambas as partes nos casos gerados.
forAll não aplica automaticamente um redutor ao gerador próprio. Para reduzir estas listas, usa forAllShrink genLista shrink; verifica sempre que o redutor conserva as condições exigidas pelo problema. Nenhuma das duas formas prova a lei para todas as listas.
Confere a tua resposta:
- Gero listas de Int no intervalo dado.
- Testo ordem e multiplicidades da saída de f.
- Dou contraexemplos distintos para perda e falta de ordenação.
Erros frequentes