O triste estado das bibliotecas de testes baseados em propriedades

 (stevana.github.io)
1 pontos por GN⁺ 2024-07-06 | 1 comentários | Compartilhar no WhatsApp
  • Testes baseados em propriedades se espalharam para várias linguagens após o QuickCheck, mas, em julho de 2024, muitas bibliotecas ainda não oferecem de forma adequada testes com estado e testes paralelos, já consolidados desde 2009
  • A lacuna principal está em verificar mudanças de estado sequenciais com um modelo de máquina de estados e reutilizar esse mesmo modelo em verificações de linearizabilidade (linearisability) para encontrar condições de corrida em execuções paralelas
  • Entre os projetos analisados, muitos não têm testes com estado ou os tratam como experimentais, e testes paralelos são ainda mais raros; FsCheck, Gopter, RapidCheck, SwiftCheck e jsverify, por exemplo, mantêm issues relacionadas abertas há anos
  • Uma implementação em Haskell com cerca de 400 linhas reproduz testes baseados em propriedades com estado e paralelismo, usando como modelo uma implementação de referência baseada em fake, mais familiar para programadores, em vez da especificação tradicional com máquina de estados
  • Um fake validado por testes de contrato pode ser reutilizado não só para verificar um componente isolado, mas também em testes de integração rápidos e determinísticos, injetado no lugar de dependências reais

A lacuna de recursos que surgiu após o QuickCheck

  • Testes baseados em propriedades se espalharam por várias comunidades de linguagens de programação sob o lema “não escreva testes, gere-os”
  • A página da Wikipedia da biblioteca original em Haskell, QuickCheck, lista 57 reimplementações em outras linguagens
  • O primeiro artigo do QuickCheck, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, foi apresentado na ICFP 2000, e todo o código-fonte da primeira implementação eram cerca de 300 linhas no apêndice do artigo
  • O QuickCheck inicial só conseguia testar funções puras; em 2002, Testing monadic code with QuickCheck estabeleceu a base para lidar com código com efeitos, como estado mutável, I/O de arquivos e rede

O surgimento dos testes com estado e paralelos

  • A Quviq AB foi fundada em 2006 por John Hughes e Thomas Arts, e um dos primeiros casos de uso foi testar o projeto Erlang da Ericsson
  • Como Erlang não é uma linguagem puramente funcional e a concorrência é comum, o QuickCheck monádico existente não era suficientemente prático por si só
  • O QuickCheck Erlang fechado da Quviq passou a incluir dois recursos que depois faltaram em várias implementações open source
    • testes baseados em propriedades com estado sequencial, usando modelos de máquina de estados
    • testes paralelos para detectar condições de corrida, reutilizando o mesmo modelo sequencial de máquina de estados
  • Testes com estado apareceram em sua forma atual em QuickCheck testing for fun and profit (2007)
  • Testes paralelos foram tratados em detalhe em Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009), usando como técnica central Linearizability: a correctness condition for concurrent objects (1990), de Herlihy e Wing
  • O código da biblioteca Quviq QuickCheck não foi compartilhado nos artigos; o que foi tornado público foram a API e exemplos de testes usando essa API

Resultados do levantamento de bibliotecas em 2024

  • O estado da arte atual é formado por testes com estado baseados em modelos de máquina de estados e testes paralelos que combinam linearizabilidade com esse mesmo modelo sequencial
  • O levantamento foi compilado a partir da leitura de documentação, issue trackers e parte do código-fonte, com base em julho de 2024
  • Muitas bibliotecas não oferecem testes com estado ou os oferecem de forma limitada
    • QuickCheck (Haskell) mantém desde 2016 uma issue para adicionar testes com estado
    • SwiftCheck também mantém desde 2016 uma issue para adicionar testes com estado
    • jsverify tem desde 2015 uma issue pendente para adicionar testes com estado
    • proptest (Rust) exige recorrer ao projeto separado proptest-state-machine
  • Suporte a testes paralelos é ainda mais raro
    • O README do Gopter diz “No parallel commands … yet?” e há uma issue de 2017
    • O FsCheck mantém desde 2016 uma issue para adicionar suporte paralelo
    • O RapidCheck mantém desde 2015 uma issue para adicionar suporte paralelo
    • O propcheck tem desde 2020 uma issue para adicionar testes paralelos
  • Como exemplos open source que oferecem os dois recursos, o texto cita PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine e stateful-check
  • Mesmo quando há recurso paralelo, às vezes há limitações
    • Um comentário no código-fonte do QuickTheories diz que, como o número possível de estados finais cresce rapidamente conforme o número de comandos, em geral é preciso limitar a command list a no máximo 10 itens
    • Os exemplos de LevelDB e Redis do ScalaCheck são apresentados como exemplos sequenciais com threadCount = 1
    • O suporte a condições de corrida no fast-check, ao contrário dos testes paralelos do Quviq QuickCheck, não parece reutilizar um modelo sequencial de máquina de estados nem usar linearizabilidade
  • Não há exemplos claros de bibliotecas que tenham adicionado testes paralelos depois; se isso não for considerado desde o desenho inicial da API, pode exigir uma reformulação significativa

Por que a disseminação desses recursos foi lenta

  • John Hughes apresentou três razões
    • testes com estado e paralelos não são tão úteis quanto testes de funções puras
    • escrever modelos de máquina de estados exige uma forma de pensar diferente dos testes comuns e requer treinamento
    • somente open source não levou bem à adoção industrial; um produto closed source e serviços de treinamento e consultoria ajudaram na adoção
  • Testar com property-based testing apenas partes puras de um sistema já traz muitos benefícios, mas sistemas industriais costumam ter banco de dados, protocolos com estado e estruturas de dados concorrentes, então testes com estado e paralelos são quase tão importantes quanto
  • Especificações com estado nem sempre são mais difíceis do que especificações de funções puras
    • Um modelo de key-value store pode ir bastante longe usando apenas uma lista de pares chave-valor
    • No caso do LevelDB, um modelo simples encontrou em poucos minutos um counterexample reduzido de 17 etapas; depois de uma correção do Google, encontrou novamente em poucos minutos um counterexample de 31 etapas
    • O segundo problema era um bug no processo de compaction em background; a compaction é importante para melhorar desempenho de leitura e recuperar espaço em disco, mas não estava incluída explicitamente no modelo
  • Embora o closed source possa ter ajudado na adoção industrial, a avaliação é que isso não ajudou a adoção open source
  • Para reproduzir os resultados dos artigos sem uma licença do Quviq QuickCheck, seria necessário muito reverse engineering, o que o texto considera quase impossível

Proposta: implementação pequena, aberta e especificações mais fáceis

  • Há duas direções de melhoria
    • fornecer uma implementação open source curta de testes baseados em propriedades com estado e paralelismo, como a implementação original do QuickCheck com cerca de 300 linhas
    • reduzir a carga de escrever especificações reutilizando, no lugar de máquinas de estados, conceitos que programadores já conhecem, como mock e test double
  • Para verificar essa hipótese, o texto mostra duas coisas
    • uma implementação de testes baseados em propriedades com estado e paralelismo em cerca de 400 linhas de código
    • o uso de uma implementation de referência em memória, isto é, um fake, como modelo no lugar de uma state machine

Resumo de testes puramente baseados em propriedades

  • Em testes de funções puras, gera-se entradas e verifica-se que a saída da função satisfaz alguma relação com a entrada
  • Por exemplo, reverse pode ser testada com a propriedade reverse (reverse xs) == xs para uma lista arbitrária xs
  • O QuickCheck gera 100 testes por padrão e, quando há falha, faz shrink da entrada para apresentar um counterexample mínimo
  • Uma propriedade incorreta como reverse xs == xs é reduzida a um contraexemplo mínimo como [0,1]
  • Padrões de propriedades que aparecem com frequência incluem inverse, idempotency, associativity, axiomas de tipos de dados abstratos e propriedades metamórficas
    • inverse: deserialise (serialise i) == i
    • idempotency: sort (sort xs) == sort xs
    • associativity: (i + j) + k == i + (j + k)

Testes baseados em propriedades com estado

  • Componentes com estado não produzem sempre a mesma saída para a mesma entrada
    • O resultado do primeiro incr de um contador e do segundo incr varia conforme o estado anterior
    • Bancos de dados e sistemas de arquivos também têm a próxima saída influenciada pelo histórico de entradas anteriores
  • Se testes de funções puras lidam com uma única entrada, testes com estado geram sequências de entrada para verificar como o sistema evolui ao longo do tempo
  • O modelo é expresso como um fake no formato m -> i -> (m, o)
    • A partir do estado anterior do modelo m e da entrada i, calcula-se o próximo modelo e a saída o
    • A saída do sistema real é comparada com a saída do fake em cada etapa
    • Se houver divergência, a sequência de entradas passa por shrink para encontrar um counterexample pequeno

  • Exemplo de contador

    • Um contador em Haskell que usa uma variável mutável global é usado como alvo de teste
    • incr incrementa o contador e get lê o valor atual
    • O modelo pode ser representado apenas com Counter Int, e a instância de StateModel define o estado inicial Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal e o gerador de comandos
    • Se for inserido um bug como incr42Bug, em que o contador não incrementa quando o valor é 42, o QuickCheck encontra a falha após 66 testes e, com 29 shrink, apresenta o contraexemplo mínimo: fazer 43 incrementos e depois Get
    • Se o contador global real não for reset entre os testes, o modelo sempre começa em 0, mas o contador real mantém o estado do teste anterior, causando mismatch

  • Interface de bibliotecas com estado

    • A interface StateModel trata o sistema sob teste como uma black box, com commands como entrada e responses como saída
    • Os componentes principais são Command state, Response state, initialState, runFake, runReal e generateCommand
    • Os componentes opcionais são os seguintes
      • Reference: usado quando um comando posterior precisa referenciar um recurso criado por uma response anterior, como um file handle
      • PreconditionFailure: expressa falhas de precondition, como impedir leitura de um handle que não está aberto
      • CommandMonad: o padrão é IO, mas outros monads podem ser usados
      • monitoring, commandName: usados para coverage e estatísticas
    • Ao gerar comandos, não é possível criar valores como um file handle real, então gera-se uma referência simbólica no formato Var Int, que é substituída por uma referência real durante a execução
    • Após o shrink, comandos que violam preconditions ou usam referências simbólicas fora de escopo são removidos

  • Exemplo de circular buffer

    • Uma circular queue escrita em C é testada via Haskell FFI, e o modelo é implementado como uma queue simples baseada em lista
    • A implementação em C não faz verificação de erros, então ao chamar get em uma queue vazia ela pode retornar memória não inicializada
    • A implementação real é eficiente por usar índice circular, mas não é obviamente correta; o fake é menos eficiente, porém isso não é problema por ser usado para teste
    • Como new retorna uma referência de queue, o modelo gerencia várias queues com Map (Var Queue) FQueue
    • No início, faltava a precondition de put em queue cheia; ao inserir 0 e 1 em uma queue de tamanho 1 e depois chamar get, o modelo espera 0 por ser FIFO, mas o código em C retorna 1
    • Isso não era um bug de implementação, mas sim a ausência de precondition no modelo, corrigida com a adição da precondition QueueIsFull
    • O fato de o comando Size não estar no generator apareceu na saída de coverage e, após adicioná-lo, foi encontrado um bug no cálculo do tamanho da queue
    • Ao inserir um item em uma queue de tamanho 1 e chamar Size, o valor esperado é 1, mas o valor real é 0; como correção, propõe-se definir o tamanho do buffer interno como n + 1 em new
    • Depois disso, abs(q->inp - q->outp) % q->size passa em filas de tamanho 1, mas falha novamente em filas de tamanho 2, e a correção final é (q->inp - q->outp + q->size) % q->size

  • O quebra-cabeça dos galões de água de Die Hard 3

    • O quebra-cabeça de obter exatamente 4L com galões de 3L e 5L é resolvido com testes baseados em propriedades com estado
    • Mesmo sem uma implementação real, executando apenas o modelo e o fake, é possível fazer o teste falhar ao atingir um estado específico e obter uma sequência de ações reduzida por shrink
    • Após 199 testes e 11 shrink, a sequência apresentada segue este fluxo
      • Encher o galão de 5L
      • Despejar do galão de 5L para o de 3L
      • Esvaziar o galão de 3L
      • Despejar novamente do galão de 5L para o de 3L
      • Encher o galão de 5L
      • Despejar do galão de 5L para o de 3L
    • O trace mostra os estados intermediários, permitindo verificar o processo em que o galão grande chega a 4L

Testes baseados em propriedades em paralelo

  • bugs em código concorrente são difíceis de reproduzir e de verificar a correção porque o interleaving das threads muda a cada execução
  • o objetivo é permitir que o usuário faça testes paralelos como nos testes sequenciais baseados em estado, sem precisar escrever muito código de teste adicional
  • no exemplo do contador, se incr executar readIORef seguido de writeIORef de forma não atômica, duas threads podem sobrescrever o incremento uma da outra, gerando uma condição de corrida
  • o teste paralelo reúne os momentos de invocação e resposta dos comandos durante a execução para criar um histórico concorrente, e verifica se esse histórico pode ser explicado por algum interleaving sequencial
  • se ao menos um interleaving for compatível com o modelo sequencial, considera-se que o histórico é linearizável e, portanto, correto
  • se nenhum interleaving sequencial conseguir explicar as respostas reais, o resultado é tratado como não linearizável

  • Geração e shrink de comandos paralelos

    • o programa paralelo é representado por ParallelCommands e vários Fork, e os comandos dentro de cada Fork são executados em paralelo
    • a implementação de exemplo lida com execução em uma, duas e três threads
    • na execução paralela, casos como Fork [Write "a" "foo", Write "a" "bar"] podem levar a estados de modelo diferentes dependendo do interleaving
    • o modelo paralelo executa a geração e o shrink de comandos com base em um conjunto de estados, e não em um único estado
    • parallelSafe verifica se a precondição é mantida em todas as permutações dos comandos dentro de um Fork
    • por exemplo, se Write "a" e Delete "a" estiverem no mesmo fork, um comando pode quebrar a precondição do outro
    • no processo de shrink, permanecem apenas os comandos que preservam a precondição e o escopo das referências simbólicas

  • Execução paralela e verificação de linearizabilidade

    • a execução paralela registra os eventos Invoke e Ok de cada comando no histórico
    • se a resposta incluir uma nova referência, o ambiente é expandido com um contador atômico para evitar colisões entre números de referência de threads diferentes
    • todos os interleavings possíveis do histórico são enumerados em uma árvore Rose
    • linearisable verifica se algum caminho dessa árvore corresponde ao modelo sequencial runFake e às respostas observadas
    • como o teste paralelo reaproveita no fim o modelo sequencial, o usuário obtém testes paralelos com pouco código extra após escrever o modelo sequencial

  • Exemplo do contador paralelo

    • o único código adicional para ativar o teste paralelo do contador foi a instância ParallelModel Counter e a property
    • ao usar o incrRaceCondition não atômico, a condição de corrida é encontrada
    • mesmo que haja uma race em um caso de teste menor, se a falha não se reproduzir por causa de outro interleaving, o QuickCheck pode considerar que esse caso menor passou e interromper o shrink
    • a solução correta é um escalonador de threads determinístico, e o artigo sobre testes paralelos usa essa abordagem
    • a implementação de exemplo usa uma solução alternativa mais simples: inserir pequenos sleeps ao redor de leituras e escritas em memória compartilhada para aumentar a chance de ocorrer o mesmo interleaving
    • o sleep não é necessário para encontrar a race, mas para reduzir o contraexemplo encontrado
    • após adicionar o sleep, o menor contraexemplo é reduzido para ParallelCommands [Fork [Incr,Incr],Fork [Get]]

  • Exemplo do registro de processos

    • usa-se como exemplo um sistema como o registro de processos do Erlang, que faz spawn de threads e registra, consulta, remove o registro e mata ThreadId por nome
    • o modelo sequencial acompanha os ids de threads criadas, os pares nome-thread registrados e os ids de threads encerradas
    • Register e Unregister podem falhar, então a resposta usa Either ErrorCall ()
    • as informações de localização do erro na implementação real são removidas com abstractError para bater com a fake
    • monitoring mostra a cobertura de RegisterFailed, RegisterSucceeded, UnregisterFailed e UnregisterSucceeded
    • ao inserir de propósito um bug em que register sobrescreve o registro existente, aparece um contraexemplo sequencial em que não é possível fazer unregister de "e" já registrado
    • no teste paralelo, surge um contraexemplo mais longo e, com SleepyIORef, ele é reduzido para a forma Fork [Register "b" (Var 0), Register "c" (Var 0)]
    • o problema é uma race em que outra thread pode intervir entre a verificação com readRegistry e a chamada a atomicModifyIORef
    • depois de aplicar um lock global a register, unregister e kill, o teste paralelo passa

Modelos baseados em fake e testes de integração

  • Em vez da especificação tradicional de máquina de estados com post-conditions, usa-se um fake em memória como implementação de referência
  • O texto de 2019 de Edsko de Vries é apresentado como o primeiro a propor uma forma de implementar um fake sobre uma especificação de máquina de estados baseada em post-conditions
  • O fake é semelhante a um mock e é apresentado como uma abordagem mais fácil para programadores não familiarizados com especificações formais
  • O fake também tem a vantagem de poder ser usado no lugar de componentes dependentes em testes de integração
    • Não é necessário iniciar nem habilitar a dependency real
    • É possível montar testes de integração mais rápidos e determinísticos
  • O problema de o fake poder estar errado é tratado com contract test
  • Como testes baseados em propriedades com estado e em paralelo verificam a correspondência entre o fake e a implementação real, o fake passa a funcionar como uma dependência testada por contrato

  • Separando teste e deploy com um fake de queue

    • A interface de queue IQueue tem iNew, iPut, iGet, iSize
    • A implementação real conecta diretamente o wrapper da queue em C
    • A implementação fake armazena o estado do modelo em IORef e o atualiza por meio de fNew, fPut, fGet, fSize
    • O componente é escrito para a interface IQueue q
    • Nos testes, usa-se a instância fake, e no deploy, a instância real
    • Assume-se, por meio de testes baseados em propriedades com estado, que o fake é fiel ao real

  • Fake de file system

    • A interface de file system IFileSystem h tem iMkDir, iOpen, iWrite, iClose, iRead
    • A implementação real usa o file system real em /tmp/qc-test
    • O fake é implementado como um FakeFS em memória com conjunto de diretórios, mapa de conteúdo dos arquivos, mapa de handles abertos e próximo handle
    • fOpen, fWrite, fClose, fRead modelam falhas de precondition, como arquivo ocupado, diretório inexistente e handle fechado
    • Se for testado que o fake de file system é fiel ao file system real, componentes que dependem do file system podem ser submetidos a testes de integração com o fake e, no deploy, trocados pelo file system real
    • Se surgirem bugs ao trocar pelo real, será preciso investigar como um mismatch entre fake e real conseguiu passar pelos testes baseados em propriedades com estado

  • Sistemas de componentes maiores

    • Um sistema em que A depende de B e B depende de C também pode ser expandido da mesma forma
    • Coloca-se uma interface em cada componente
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • A estratégia de teste é a seguinte
      • C é validado com testes baseados em propriedades com estado e em paralelo para obter um fake C testado por contrato
      • Nos testes de integração de B, usa-se o fake C
      • Nos testes de A, usa-se um fake B que utiliza o fake C
    • Essa abordagem também se estende ao mesmo padrão para mais componentes ou serviços

Conclusão

  • Testes baseados em propriedades com estado e em paralelo podem ser implementados com cerca de 400 linhas de código, uma escala comparável à primeira implementação do QuickCheck, que tinha cerca de 300 linhas e não fazia shrinking
  • Usar fake como modelo torna a escrita de especificações para testes com estado e em paralelo mais próxima de um formato familiar, além de permitir reutilização ao testar sistemas maiores de forma composicional
  • Se cada comunidade de linguagem continuar experimentando, ainda há espaço para melhorar o estado das bibliotecas de testes baseados em propriedades

Leituras relacionadas

1 comentários

 
GN⁺ 2024-07-06
Opiniões no Hacker News

  • O fuzzing baseado em cobertura surgiu e também tem bom suporte em Go; fico curioso para saber o que se perde ao não usar uma biblioteca de testes baseados em propriedades
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    Olhando para o teste de fuzz abaixo e a verificação de invariantes correspondente, parece que, na prática, é quase a mesma coisa que testes de propriedades
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • A distinção entre testes baseados em propriedades e fuzzing é, em geral, mais uma classificação aproximada por estilo
      Existem diferenças reais, mas a fronteira é bastante nebulosa, e não é tão importante separar com precisão o que é fuzzing e o que é teste baseado em propriedades
      Testes rápidos com asserções detalhadas são testes baseados em propriedades; rodar por muito tempo procurando apenas crashes é fuzzing; o que fica no meio é ambíguo
      https://hypothesis.works/articles/what-is-property-based-tes...
    • Fuzzing baseado em cobertura e testes baseados em propriedades podem muito bem ser combinados
      Quando eu estava no Google, havia uma ferramenta interna que combinava os dois e era realmente boa. Você escrevia testes baseados em propriedades como de costume e, na execução, o framework de testes compilava de forma especial para obter cobertura e ajustava as entradas aleatórias para aumentá-la. Claro, isso rodava de modo totalmente automático em um cluster com várias máquinas
      Testes baseados em propriedades tradicionais normalmente são implementados apenas como bibliotecas, portanto nem sempre há informações de cobertura para orientar a geração de entradas aleatórias
    • Como há asserções sobre propriedades, eu consideraria isso, por definição, um teste baseado em propriedades, como em “todo nó com nível maior que 1 tem dois filhos”
      Dito isso, dependendo da biblioteca, dá para obter bastante conveniência. Uma funcionalidade desejável é o shrinking, e a seção “Shrinking” aqui serve de referência: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      Combinators para compor geradores também são excelentes, e algumas bibliotecas têm conjuntos conhecidos de valores “ruins” que provocam comportamentos excepcionais
    • Não sei bem em que os testes de fuzz do Go diferem do conteúdo do artigo linkado, mas nele se dizia que um fuzzer de verdade deve rodar por dias ou semanas, e que testes baseados em propriedades quase sempre devem ser escolhidos em vez de fuzzing
      Quero dar um passo atrás e fazer uma pergunta mais meta sobre testes. Sucesso nos testes significa sucesso do código, e o contrário também vale? Há alguma parte do contrato do Go que especifique que, ao passar a mesma entrada para o mesmo código, a mesma saída será produzida?
    • Do ponto de vista de API, o principal ganho é uma biblioteca de combinators para gerar as estruturas de dados aleatórias desejadas
      Ao trabalhar com o tipo Arbitrary, que representa um conjunto de objetos aleatórios, fica fácil escrever funções reutilizáveis que geram entradas de teste. Parece que esse tipo de biblioteca também poderia ser usado com bastante facilidade junto ao framework de fuzzing do Go
      Ainda assim, acho que combinators comuns como map, filter, chain e oneOf podem ficar um pouco estranhos, então estou escrevendo uma nova biblioteca de testes de propriedades para JavaScript. O objetivo é torná-la mais agradável de usar, mas ela ainda é experimental e não foi publicada

  • clojure.spec.alpha foi uma ótima experiência, usando junto com test.check ou não, mas ao experimentar o hypothesis do Python achei realmente péssimo
    O Hypothesis parecia incapaz, por design, de lidar com conjuntos de dados simples porém “grandes” — e, aqui, “grande” nem era tão grande assim. [0] Foi tão doloroso que removi completamente o Hypothesis e os testes baseados em geração da suíte de testes em Python do trabalho
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • Neste caso, soa menos como o Hypothesis não conseguir lidar com conjuntos de dados grandes e mais como se ele estivesse rejeitando muitos dos casos reduzidos
      O Hypothesis tentou reduzir os inteiros gerados para 0 para ver se o bug também existia em 0, e o teste, por conter 0, rejeitou o caso em vez de falhar. Em casos pequenos isso foi apenas ineficiente, mas em casos grandes chegou a ponto de o Hypothesis desistir
      Naquela thread, alguém sugeriu usar uma estratégia diferente de geração de instâncias que não pudesse gerar 0. Ou seja, não gerar o valor favorito do redutor do Hypothesis para depois rejeitá-lo, mas evitar criá-lo desde o início. Fico curioso se tentaram isso
      Também fico curioso sobre como clojure.spec.alpha trata isso de forma diferente
      O comentário de mjaniczek em https://news.ycombinator.com/item?id=40876437 aponta este caso como uma desvantagem da abordagem do Hypothesis
      A ideia é algo como: “há um pouco de ineficiência, porque o gerador agora vira um parser de listas de bytes que pode falhar, e o usuário pode criar geradores estranhos que o redutor interno não consegue reduzir perfeitamente. Ainda assim, entre as três abordagens, é a que oferece a melhor experiência para o desenvolvedor…”
      Claro que a própria pessoa provavelmente não concordaria que escreveu o teste de um jeito “estranho”
    • O spec do Clojure era ótimo porque era muito fácil montar o entorno, mas, ao mudar para Elixir, para escrever esse tipo de teste precisei descer até uma biblioteca antiga de Erlang, a propEr. Foi bem decepcionante
    • O exemplo no issue do GitHub usa filter de uma forma que causa o próprio problema
      Se você gera aleatoriamente e depois filtra o que se encaixa em alguma propriedade, na prática está raspando uma raspadinha durante o processo de geração

  • A resposta simples à pergunta do texto — “por que não há uma exigência de que pesquisas publicadas sejam reprodutíveis com ferramentas open source, ou pelo menos com ferramentas disponibilizadas gratuitamente ao público e a outros pesquisadores?” — é que a consequência imediata dessa exigência seria que artigos que não atendessem a essa condição não seriam publicados
    Por exemplo, até o artigo sobre o Quviq QuickCheck, que parece ter sido útil para os autores e para outras pessoas, talvez não tivesse sido publicado, e a comunidade teria perdido esse presente em forma de informação

    • Seria bom se algumas editoras exigissem reprodutibilidade e outras não
      Toda exigência tem efeito de exclusão, e sempre há casos de fronteira de artigos que podem ser úteis mesmo sem cumprir determinado requisito
    • Esta não é uma questão com uma resposta claramente delimitada — dá até para chamá-la de uma questão política —, mas isso não torna essa linha de defesa muito válida
      Se aceitarmos esse raciocínio como válido, ele pode ser usado como escudo para ir até qualquer ponto. Se removemos a reprodutibilidade dos requisitos, então não é preciso explicar nada que não se queira explicar. Não é necessário fornecer dados sobre a amostra nem testes de significância estatística. Um resumo vago afirmando que algum resultado foi alcançado já passa a ser suficiente
      Até a famosa anotação que Fermat deixou na margem de seu exemplar pessoal de Arithmetica se tornaria um artigo de pesquisa totalmente válido. Afinal, não queremos perder a valiosa informação de que um matemático famoso achava ter uma demonstração concisa e elegante de um teorema. Claro que, na prática, é bem provável que ele não tivesse
      Minha opinião sobre essa questão política é que os critérios atuais são frouxos demais. Ninguém é obrigado a publicar nada. Há muita pesquisa no mundo que não é publicada em lugar nenhum por razões como valor proprietário, e esse tipo de pesquisa não vai desaparecer
      Mas, se alguém trabalha na academia — ainda mais recebendo financiamento de pesquisa — e diz que seu objetivo é fazer avançar o conhecimento científico do mundo, então é justo exigir que de fato siga esse objetivo. Não apenas finja segui-lo para subir na carreira acadêmica
    • Talvez fosse possível disponibilizar o código-fonte apenas aos revisores
      Junto com tudo o que for necessário para executar o código. Talvez isso já esteja sendo feito
    • Porque reprodutibilidade é uma pedra angular do método científico
    • Artigos são publicados porque seus autores querem aumentar seu “índice de importância”, algo que está muito diretamente ligado à remuneração e às possibilidades de carreira acadêmica
      Para esse objetivo, é improvável que acrescentar mais requisitos reduza o número de artigos publicados
      O problema mais sério dos artigos publicados é que, com frequência, erros são ignorados deliberadamente para publicar o máximo possível, o mais rápido possível. Se ficar mais fácil verificar artigos, talvez essa situação melhore, mas eu não criaria grandes expectativas. As pessoas são muito boas em encontrar atalhos

  • Escrevo testes de propriedades com estado com bastante frequência usando proptest em Rust e, em geral, programá-los à mão é bem simples
    Um exemplo não trivial que encontrou 6 bugs está em https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    Testes paralelos podem ser úteis às vezes, mas muitas vezes é mais fácil simplesmente rodar muitos testes em paralelo

    • Escrevo muitos testes de propriedades manuais em Rust, e em geral eles têm este formato
      No nível mais alto, uso aleatoriedade de verdade e, abaixo disso, coloco vários loops aninhados para ir de casos de baixa complexidade a casos de alta complexidade. Em seguida, gero e imprimo uma semente para passar a um gerador pseudoaleatório determinístico. Se o teste falhar, basta copiar e colar a semente do erro para reproduzir o caso de falha
      Senti que esses testes de propriedades manuais são mais rápidos, mais flexíveis e, no geral, dão menos trabalho do que qualquer framework ou biblioteca
      Dito isso, para testes de concorrência realmente robustos, recomendo fortemente a biblioteca AWS Shuttle (https://github.com/awslabs/shuttle). Ela consegue encontrar condições de corrida incrivelmente complexas. Também escrevi um pequeno tutorial: https://grantslatton.com/shuttle
      Na AWS, usamos essa biblioteca para validar um sistema de arquivos personalizado escrito para rodar o AWS S3

  • Dei uma olhada rápida no artigo linkado “Testing Telecoms Software with Quviq QuickCheck”, mas não vi de imediato uma resposta para a pergunta “por que não seria melhor criar essas operações com estado diretamente?”
    O texto original aponta para isso com um modelo de pares chave-valor de um armazenamento chave-valor, mas não entendo por que não simplesmente escrever uma máquina de estados, nem por que um framework seria necessário. Na semana passada, no trabalho, fiz literalmente isso para testar interações com um sistema de arquivos, e no fim se resumiu a algo como type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
    Então a propriedade vira “dada esta lista de comandos, …”. O formato StateModel basicamente exige a mesma coisa. É difícil ver o StateModel fazendo sua parte; parece que ele só elimina uma quantidade muito pequena de código de teste na prática, ao custo de acrescentar muito mais código de framework que precisa ser entendido

    • Há testes em que esse julgamento está certo, mas a parte de reduzir os casos de falha costuma ser complicada
      Se você quer gerar apenas sequências “válidas” de transições de estado, normalmente precisa de um estado de modelo que determine quais etapas de teste são válidas em determinado estado. Além disso, é preciso evitar que, durante a redução, a remoção de etapas de teste quebre as pré-condições que foram respeitadas quando cada etapa foi gerada originalmente, criando falhas falsas
      Se você só quer uma sequência de operações arbitrária e totalmente aleatória, em que qualquer operação é válida em qualquer estado, um framework proptest com estado pode ser exagero. Mas, se você precisa manter um estado de modelo e especificar pré-condições para várias operações, um framework dedicado poupa bastante trabalho
      Escrevi um post no blog sobre esse tema no ano passado; se quiser um exemplo mais aprofundado, vale consultar: https://readyset.io/blog/stateful-property-testing-in-rust
      Como outras pessoas disseram, testes de máquina de estados paralelos também são um benefício interessante que se pode obter de um framework dedicado, mas não são o único benefício
    • Acho que a parte com estado é tratada melhor por testes baseados em modelo
      Dá para misturar estilos de teste. O código é seu
    • Entendo que o QuickCheck paralelo verifica se todos os interleavings possíveis em um programa multithread produzem, ao final, um estado que também seria alcançável ao chamar os comandos sequencialmente
      Essa é a vantagem

  • O autor se concentra nos aspectos de máquina de estados e paralelismo dos testes baseados em propriedades, mas também há outros aspectos que podem ter um impacto maior
    Um deles é o teste baseado em propriedades guiado por cobertura, e basta ver o texto de Dan Luu: https://danluu.com/testing/
    Outro, para o qual sou tendencioso, é automatizar o shrinking mantendo todas as invariantes criadas ao gerar os valores
    Em resumo, funções de shrinking derivadas no estilo QuickCheck que operam sobre valores (shrink : a -> [a]) têm restrições e problemas, então as pessoas acabam desativando o shrinking em vez de lidar com o problema
    O “shrinking integrado” com rose trees (por exemplo, Hedgehog) segue as restrições do gerador, mas tem problemas com monadic bind, isto é, quando se usa o resultado de um gerador para ramificar para outro gerador
    A única abordagem que parece magicamente “simplesmente funcionar” é o shrinking interno do Hypothesis. Ela usa uma camada indireta que reduz uma lista de escolhas aleatórias, não o valor em si. A desvantagem é que o gerador passa a ser um parser de lista de bytes que pode falhar, o que traz certa ineficiência, e o usuário pode criar geradores estranhos que o shrinker interno não consegue reduzir perfeitamente. Ainda assim, entre as três abordagens, ela tem a melhor experiência para o desenvolvedor e, considerando que o simples fato de as pessoas escreverem testes já é um pequeno milagre, parece ser a abordagem que mais vale a pena construir como autor de uma biblioteca de testes

    • Sobre a parte em que o “shrinking integrado” com rose trees (por exemplo, Hedgehog) segue as restrições do gerador, mas tem problemas com monadic bind: dentro dos limites do meu conhecimento amador, vejo isso como uma limitação fundamental do monadic bind/gerador
      Em vez disso, para obter shrinking ideal, deve-se preferir geradores applicative: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      Em outras palavras, geradores applicative não “usam o resultado de um gerador para ramificar para outro gerador”, e o shrinking é otimizado devido ao caráter “paralelo” do applicative. Aqui, paralelo não é no sentido de threads do texto, mas no sentido monádico. Como applicative é “paralelo”, os geradores podem ser reduzidos independentemente. Já geradores monádicos são “seriais”, então reduzir um necessariamente muda o comportamento do gerador que vem depois
      Se houver uma apresentação pública, gostaria de ver o link
    • Pessoalmente, Hypothesis esteve longe de “simplesmente funcionar” para mim
      Não acho que esteja realmente pronto para produção, e isso também parece ser algo de projeto.[0]
      Como tenho bastante experiência usando clojure.spec.alpha com e sem test.check, eu não estava completamente alheio à ideia geral, ainda que haja diferenças
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • Meu framework preferido é o falsify, que oferece “shrinking integrado interno”
      Ele é parecido com o Hypothesis, mas usa uma árvore de geração em vez de uma sequência linear. É baseado em selective functor, que é uma boa interface também útil para coisas como validadores
      Segundo https://hackage.haskell.org/package/falsify, essa biblioteca oferece testes baseados em propriedades com suporte a shrinking integrado interno. Integrado no sentido do Hedgehog, ou seja, não é preciso escrever um shrinker e um gerador separados; e interno no sentido do Hypothesis, ou seja, também funciona bem em todo o monadic bind

  • Tentei usar testes baseados em propriedades, mas sempre tive a sensação de estar entre duas cadeiras
    Se eu entendo uma propriedade bem o bastante para testá-la rigorosamente, em geral posso empurrá-la para o sistema de tipos e torná-la verdadeira por construção. Se eu só quero um teste de fumaça simples, uma única entrada arbitrária é mais fácil

    • Fico curioso para saber que tipo de propriedade você tem em mente
      Por exemplo, muitas vezes há duas implementações, uma ingênua, lenta mas simples, e outra otimizada, e é possível comparar as saídas das duas para entradas arbitrárias. É uma propriedade simples e fácil de entender, mas geralmente difícil de colocar no sistema de tipos
      Da mesma forma, pode haver a propriedade de que a ordem em que as entradas são apresentadas não deveria importar, ou de que há uma forma de dividir os dados tal que max(valor máximo de A, valor máximo de B) = maximum(A union B). Como codificar isso no sistema de tipos?
      Ou algo como “para quaisquer A e B, alguma solução ótima encontrada em A é pior do que alguma solução ótima encontrada em A union B”, ou ainda idempotência como f(f(A)) = f(A)
      Todas essas são propriedades fáceis de entender, mas não são fáceis de expressar na maioria dos sistemas de tipos
    • Se possível, claramente é melhor impor restrições em tempo de compilação
      Mas há muitas restrições que os verificadores de tipos mainstream não conseguem tratar. Tipos dependentes ajudariam bastante, mas ainda parecem restritos a nichos como provadores de teoremas

  • Pergunto-me se a lista não deixou de fora o QuviQ Erlang QuickCheck original
    O produto completo é proprietário, mas também há uma versão gratuita, o QuickCheck Mini: http://www.quviq.com/downloads/

  • Clojure agora também tem uma biblioteca quickcheck com estado: https://github.com/griffinbank/test.contract
    Testes paralelos são interessantes, mas ainda não foram uma grande fonte de dor

  • Em testes em C#/.NET, tenho usado CsCheck[0] e fiquei bastante satisfeito
    Era muito mais acessível do que Hedgehog ou FsCheck, e também bem rápido
    [0] https://github.com/AnthonyLloyd/CsCheck