Propriedades e testes com QuickCheck

Propriedades em vez de exemplos

Um exemplo verifica uma entrada; uma propriedade afirma algo sobre uma família de entradas. O QuickCheck gera casos e procura uma violação. Passar os casos gerados não prova a afirmação universal.

import Test.QuickCheck

prop_revRev :: [Int] -> Bool
prop_revRev xs = reverse (reverse xs) == xs

ghci> quickCheck prop_revRev
+++ OK, passed 100 tests.

• Os casos podem incluir listas vazias, negativos e repetidos. Só os casos gerados foram observados.
• Os 100 casos são a omissão da ferramenta; podes pedir mais com argumentos de configuração.

O contrato antes da propriedade

Uma função de ordenação deve produzir uma lista ordenada com os mesmos elementos e multiplicidades. Em [2,1,2], devolver [1,2] perde uma ocorrência; devolver [2,1,2] não ordena.

• A idempotência f (f xs) == f xs verifica outra lei. f xs = [] satisfaz essa igualdade e perde os dados: caracteriza a ordenação pela ordem e pela conservação das multiplicidades.
• Com uma implementação de referência independente, compara os resultados.

Contraexemplos e shrinking

prop_sortId :: [Int] -> Bool
prop_sortId xs = sort xs == xs

ghci> quickCheck prop_sortId
*** Failed! Falsifiable (after 3 tests):
[1,0]

• A testemunha [1,0] mostra que a propriedade é que está errada, não a ordenação: compara o contraexemplo com o contrato antes de mudar a implementação.
• O shrinking tenta reduzir a entrada conservando a falha; as reduções disponíveis não garantem o mínimo global.

Geradores e pré-condições

prop_divMod :: Integer -> Integer -> Property
prop_divMod x y = y /= 0 ==> (x `div` y) * y + (x `mod` y) == x

• Com ==>, os casos com y == 0 são descartados e não contam como testes. Se a pré-condição for rara, a ferramenta pode desistir sem a amostra pedida.
• Um gerador à medida constrói entradas válidas em vez de descartar: gera pares já ordenados para testar o máximo do par.
• suchThat repete tentativas até satisfazer a condição; uma condição rara pode impedir a geração. forAll não reduz entradas próprias: usa forAllShrink com redutor que preserve a condição.
• Para insert x xs com xs ordenada por contrato, ordena a lista gerada antes de testar.

Um contraexemplo no papel

A lei reverse (xs ++ ys) == reverse xs ++ reverse ys é falsa: com xs=[1] e ys=[2], dá [2,1] contra [1,2]. A lei correta troca a ordem: reverse (xs ++ ys) == reverse ys ++ reverse xs.

Para justificar uma propriedade, identifica ainda o domínio. A igualdade com length pressupõe listas finitas; leis em Int podem sofrer overflow. Usa Integer na aritmética exata para não confundir matemática com representação.