Oráculos de corretude
Escolha uma observação que possa refutar o comportamento prometido. Especifique o que uma verificação bem-sucedida deixa não testado: uma comparação de contagem, verificação estrutural e testemunha de dependência observam propriedades diferentes (implementação NoREC, verificações de integridade do SQLite, Elle §4.3).
Derive a verificação a partir do limite real
Leia a configuração habilitada do alvo, o produtor público e o contrato governante. Identifique estados iniciais legais, pré-condições de operação, erros permitidos e o limite prometido: uma operação, statement, transação, recuperação ou histórico observado. No SQLite, ABORT desfaz um statement, enquanto uma chave estrangeira adiada "não é verificada até que a transação tente COMMIT" (ABORT do SQLite, chaves estrangeiras adiadas). Consulte as configurações efetivas quando possível; a configuração de chave estrangeira do SQLite, por exemplo, "é um no-op dentro de uma transação" (foreign_keys do SQLite).
Escreva uma observação candidata concreta antes de escalar a busca:
- Promessa: o resultado ou efeito exato proibido, com sua citação do contrato.
- Observação: conteúdo retornado real, estado ou testemunha que distingue essa violação do comportamento permitido.
- Pré-condições e pontos cegos: configuração suportada, estado válido, informação omitida e execuções indistinguíveis.
- Evidência de reprodução: entrada e estado inicial, sequência de operações, configuração efetiva e observações brutas.
Esta é uma convenção de design compacta, não um esquema obrigatório. Seu propósito é expor informações perdidas pela verificação proposta; o modelo de observação de Elle mostra por que dependências ocultas não podem ser recuperadas meramente gerando mais históricos: escritas cegas em registradores "destroem o histórico" (Elle §§3–4.3). Leia exemplos de contrato para limites trabalhados.
Em JavaScript, um código de saída do processo, status do test runner ou console limpo é tal observação: seu significado depende do modo efetivo, listeners instalados, configuração do runner e build. Com um handler uncaughtException instalado, o processo Node "sairá com 0" a menos que o handler defina process.exitCode (Node process, uncaughtException). Leia canais de observação JavaScript para canais Node, test runner, React e Playwright.
Mantenha a observação independente do comportamento suspeito
Rastreie como o valor esperado ou invariante é obtido. Identifique código compartilhado e suposições que poderiam fazer o alvo e o verificador concordarem na mesma resposta errada. Prefira um modelo abstrato justificado, invariante especificado independentemente ou relação válida sobre um algoritmo de produção copiado. Uma segunda implementação é uma opção: o SQL Logic Test do SQLite executa statements contra vários motores e verifica "se todos obtêm as mesmas respostas". Uma relação no mesmo motor é outra: o SQLite executa suítes com otimizações desabilitadas, e o NoREC do SQLancer compara uma consulta otimizada com uma não otimizada (testes do SQLite §2, §9, implementação NoREC).
Meça a informação realmente comparada. Contagens iguais de linhas não estabelecem identidade de linhas; um integrity_check saudável não estabelece integridade referencial, porque "não encontra erros de FOREIGN KEY". Preserve verificações parciais válidas e adicione uma observação complementar apenas quando a garantia do alvo exigir (implementação NoREC, verificações de integridade do SQLite). Leia observações parciais ao escolher uma referência, normalização ou testemunha.
Verifique erros permitidos e seus efeitos
Derive o pós-estado permitido separadamente do status retornado. ABORT e FAIL do SQLite ambos retornam um erro de restrição, mas ABORT desfaz o statement com falha enquanto FAIL "não desfaz alterações anteriores do SQL statement que falhou". Uma asserção apenas de erro pode perder um efeito errado; uma asserção genérica de rollback pode rejeitar comportamento legal (políticas de conflito do SQLite).
Selecione um observador para a promessa real, com pré-condições válidas. Para verificações referenciais do SQLite, use a observação de chave estrangeira aplicável, configuração de fiscalização efetiva e semântica NULL legal; não substitua por um resultado genérico de integridade (chaves estrangeiras do SQLite, foreign_key_check). Estes são contratos trabalhados, não padrões para APIs arbitrárias.
Preserve o resultado da verificação e seus limites
Distinga propriedades avaliadas de entradas rejeitadas, erros esperados, verificações ignoradas e observações insuficientes sempre que essa diferença afetar a conclusão. NoREC pula uma comparação quando qualquer contagem é seu sentinela -1 (por exemplo, após um erro de consulta esperado) em vez de contá-la como igualdade, e relata um erro inesperado como falha. A completude de Elle depende da informação registrada, e "observações raramente são completas" (implementação NoREC, Elle §4.3).
Use harness-sensitivity para estabelecer que a observação atinge e rejeita uma violação representativa justificada independentemente. Mantenha a testemunha bruta para evidence-based-triage: a própria documentação de Elle recomenda "verificar anomalias relatadas manualmente" em vez de tratar o rótulo como autoridade final (README do Elle). A alocação geral de busca pertence a bugfinding-campaign.
Direcione o raciocínio especializado escolhido para semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing ou liveness-testing; esta habilidade detém a decisão de contrato-para-observação. Leia erros comuns para atalhos enganosos.
Retorne o oráculo utilizável
Retorne o produtor, garantia citada, pré-condições efetivas, observação executável e interpretação do resultado, com uma distinção trabalhada de permitido/proibido. Declare o que permanece não observável e que evidência deve sobreviver à reprodução. Uma contradição testemunhada suporta apenas a garantia e suposições realmente verificadas (Elle §§4.3 e 9).