Aprenda como o trabalho de Tony Hoare sobre lógica de Hoare, Quicksort e pensamento de segurança moldou técnicas práticas para escrever e revisar software correto.
Quando as pessoas dizem que um programa é “correto”, muitas vezes querem dizer: “Eu rodei algumas vezes e a saída parecia certa.” Isso é um sinal útil — mas não é corretude. Em termos simples, corretude significa que o programa atende à sua especificação: para toda entrada permitida, produz o resultado exigido e respeita quaisquer regras sobre mudanças de estado, tempo e erros.
O problema é que “atende à especificação” é mais difícil do que parece.
Primeiro, especificações costumam ser ambíguas. Um requisito de produto pode dizer “ordenar a lista”, mas isso quer dizer ordenação estável? E valores duplicados, listas vazias ou itens não numéricos? Se a especificação não disser, pessoas diferentes assumirão respostas diferentes.
Segundo, casos de borda não são raros — são apenas menos frequentemente testados. Valores nulos, estouro, limites off-by-one, sequências de usuário incomuns e falhas externas inesperadas podem transformar “parece funcionar” em “falhou em produção”.
Terceiro, requisitos mudam. Um programa pode ser correto relativamente à especificação de ontem e incorreto relativamente à de hoje.
A grande contribuição de Tony Hoare não foi a afirmação de que devemos provar tudo o tempo todo. Foi a ideia de que podemos ser mais precisos sobre o que o código deve fazer — e raciocinar sobre isso de forma disciplinada.
Neste post, seguiremos três fios conectados:
A maioria das equipes não escreverá provas formais completas. Mas mesmo o pensamento “no estilo prova” parcial pode facilitar achar bugs, tornar revisões mais afiadas e esclarecer o comportamento antes do código ser entregue.
Tony Hoare é um daqueles raros cientistas da computação cujo trabalho não ficou restrito a artigos ou salas de aula. Ele transitou entre academia e indústria, e se preocupou com uma pergunta prática que toda equipe ainda enfrenta: como sabemos que um programa faz o que pensamos que ele faz — especialmente quando o risco é alto?
Este artigo foca em algumas ideias de Hoare que aparecem com frequência em codebases reais:
{P} C {Q}.Você não encontrará formalismo matemático profundo aqui, e não tentaremos uma prova completa verificável por máquina do Quicksort. O objetivo é manter os conceitos acessíveis: estrutura suficiente para clarear seu raciocínio, sem transformar sua revisão de código em um seminário de pós-graduação.
As ideias de Hoare se traduzem em decisões ordinárias: de que suposições uma função depende, o que ela garante aos chamadores, o que deve se manter verdadeiro no meio de um laço e como perceber mudanças “quase corretas” durante as revisões. Mesmo quando você nunca escreve {P} C {Q} explicitamente, pensar nessa forma melhora APIs, testes e a qualidade das discussões sobre código complexo.
A visão de Hoare é mais estrita que “passou em alguns exemplos”: corretude é cumprir uma promessa acordada, não apenas parecer certo em uma amostra pequena.
Bugs frequentemente ocorrem quando equipes pulam a etapa do meio: saltam dos requisitos diretamente para o código, deixando a “promessa” vaga.
Duas reivindicações diferentes frequentemente se confundem:
Para sistemas reais, “nunca terminar” pode ser tão prejudicial quanto “terminar com a resposta errada.”
Declarações de corretude nunca são universais; dependem de suposições sobre:
Ser explícito sobre as suposições transforma “funciona na minha máquina” em algo com que outros podem raciocinar.
Considere uma função sortedCopy(xs).
Uma especificação útil poderia ser: “Retorna uma nova lista ys tal que (1) ys está ordenada em ordem ascendente, e (2) ys contém exatamente os mesmos elementos que xs (mesmas contagens), e (3) xs não foi alterada.”
Agora “correto” significa que o código satisfaz esses três pontos sob as suposições declaradas — não apenas que a saída parecia ordenada em um teste rápido.
A lógica de Hoare é uma maneira de falar sobre código com a mesma clareza que você usaria ao falar sobre um contrato: se você começa num estado que satisfaz certas suposições, e executa este trecho de código, você terminará num estado que satisfaz certas garantias.
A notação central é a tripla de Hoare:
{precondition} program {postcondition}
Uma precondição declara o que deve ser verdade antes do fragmento de programa ser executado. Isso não é sobre o que você espera que seja verdade; é o que o código precisa que seja verdade.
Exemplo: suponha uma função que retorna a média de dois números sem checagens de overflow.
a + b cabe no tipo inteiroavg = (a + b) / 2avg é igual à média matemática de a e bSe a precondição não se mantém (há risco de overflow), a promessa da postcondição deixa de valer. A tripla força você a dizer isso em voz alta.
Uma postcondição declara o que será verdade após a execução do código — assumindo que a precondição foi satisfeita. Boas postcondições são concretas e verificáveis. Em vez de “resultado é válido”, diga o que “válido” significa: ordenado, não-negativo, dentro dos limites, inalterado exceto por campos específicos etc.
A lógica de Hoare escala de afirmações minúsculas a código multi-etapas:
x = x + 1, que fatos sobre x são verdadeiros?O objetivo não é espalhar chaves {} por todo o código. É tornar a intenção legível: suposições claras, resultados claros e menos conversas “parece funcionar” em revisões.
Um invariante de laço é uma afirmação que é verdadeira antes do laço começar, continua verdadeira após cada iteração e permanece verdadeira quando o laço termina. É uma ideia simples com grande benefício: substitui “parece funcionar” por uma afirmação que você pode checar a cada passo.
Sem invariante, uma revisão costuma soar como: “Percorremos a lista e gradualmente consertamos coisas.” Um invariante força precisão: o que exatamente já está correto agora, mesmo que o laço não tenha terminado? Uma vez que você consiga dizer isso com clareza, erros off-by-one e casos faltantes ficam mais fáceis de detectar, porque aparecem como momentos em que o invariante seria violado.
A maior parte do código do dia a dia pode usar alguns modelos confiáveis.
1) Limites / segurança de índices
Mantenha índices em intervalo seguro.
0 <= i <= nlow <= left <= right <= highEsse tipo de invariante é ótimo para prevenir acessos fora do intervalo e para tornar o raciocínio sobre arrays concreto.
2) Itens processados vs. não processados
Separe seus dados em uma região “feito” e uma “ainda não” processada.
a[0..i) foram examinados.”result satisfaz o predicado do filtro.”Isso transforma progresso vago em um contrato claro sobre o que “processado” significa.
3) Prefixo ordenado (ou prefixo particionado)
Comum em ordenação, mesclagem e partição.
a[0..i) está ordenado.”a[0..i) são <= pivot, e todos os itens em a[j..n) são >= pivot.”Mesmo que o array inteiro ainda não esteja ordenado, você definiu o que já está.
Corretude não é só estar certo; o laço também precisa terminar. Uma forma simples de argumentar isso é nomear uma medida (chamada de variant) que diminui a cada iteração e não pode diminuir para sempre.
Exemplos:
n - i encolhe em 1 a cada vez.”Se você não encontrar uma medida que encolha, pode ter descoberto um risco real: loop infinito em algumas entradas.
Quicksort tem uma promessa simples: dada uma fatia (ou segmento de array), rearranje seus elementos para que fiquem em ordem não decrescente, sem perder ou inventar valores. A forma de alto nível do algoritmo é fácil de resumir:
É um ótimo exemplo didático para corretude porque é pequeno o suficiente para caber na cabeça, mas rico o bastante para mostrar onde o raciocínio informal falha. Um Quicksort que “parece funcionar” em alguns testes aleatórios ainda pode estar errado de formas que só aparecem com entradas específicas ou casos de borda.
Alguns problemas causam a maioria dos bugs:
Para argumentar corretude no estilo Hoare, normalmente você separa a prova em duas partes:
Essa separação mantém o raciocínio manejável: acerte a partição, depois construa a corretude da ordenação sobre ela.
A velocidade do Quicksort depende de uma rotina aparentemente pequena: partition. Se a partição estiver minimamente errada, o Quicksort pode ordenar mal, entrar em loop infinito ou travar em casos de borda.
Usaremos o clássico esquema de partição de Hoare (dois ponteiros movendo-se para dentro).
Entrada: um segmento do array A[lo..hi] e um valor pivot escolhido (frequentemente A[lo]).
Saída: um índice p tal que:
A[lo..p] é <= pivotA[p+1..hi] é >= pivotNote o que não é prometido: o pivô não precisa terminar necessariamente em p, e elementos iguais ao pivô podem aparecer em qualquer dos lados. Isso é aceitável — o Quicksort só precisa de uma divisão correta.
Enquanto o algoritmo avança com dois índices — i pela esquerda e j pela direita — um bom raciocínio foca no que já está “consolidado”. Um conjunto prático de invariantes é:
A[lo..i-1] são <= pivot (lado esquerdo limpo)A[j+1..hi] são >= pivot (lado direito limpo)A[i..j] está não classificado (ainda a ser verificado)Quando encontramos A[i] >= pivot e A[j] <= pivot e trocamos, preservamos esses invariantes e reduzimos o meio não classificado.
i corre para a direita; a partição ainda deve terminar e retornar um p sensato.j corre para a esquerda; mesma preocupação de terminação.< vs <=), ponteiros podem travar. O esquema de Hoare depende de uma regra consistente para que haja progresso.Existem diferentes esquemas de partição (Lomuto, Hoare, partição em três vias). O importante é escolher um, declarar seu contrato e revisar o código com base naquele contrato de forma consistente.
Recursão é mais fácil de confiar quando você consegue responder duas perguntas claramente: quando ela para? e por que cada passo é válido? O pensamento no estilo Hoare ajuda porque força você a declarar o que deve ser verdade antes de uma chamada e o que será verdade depois que ela retornar.
Uma função recursiva precisa de ao menos um caso base onde não faz mais chamadas recursivas e ainda satisfaz a promessa dada. Para ordenação, um caso base típico é “vetores de tamanho 0 ou 1 já estão ordenados.” Aqui, “ordenado” deve ser explícito: para uma relação de ordenação ≤, o array de saída é ordenado se para todo índice i < j temos a[i] ≤ a[j]. (Se elementos iguais mantêm a ordem original é uma propriedade separada chamada estabilidade; Quicksort normalmente não é estável a menos que você o projete para isso.)
Cada passo recursivo deve chamar a si mesmo com uma entrada estritamente menor. Esse “encolhimento” é seu argumento de terminação: se o tamanho diminui e não pode ficar abaixo de zero, não é possível recursar para sempre.
O encolhimento também importa para segurança de pilha. Mesmo código correto pode travar se a profundidade de recursão ficar muito alta. No Quicksort, partições desbalanceadas podem produzir recursão profunda. Isso é um argumento de terminação e um lembrete prático para considerar a profundidade no pior caso.
O pior caso do Quicksort pode degradar para O(n²) quando partições são muito desbalanceadas, mas isso é uma preocupação de desempenho — não de corretude. O objetivo do raciocínio aqui é: assumindo que a partição preserva elementos e os divide segundo o pivô, ordenar recursivamente as partes menores implica que a faixa inteira satisfaz a definição de ordenação.
Testes e raciocínio no estilo prova buscam o mesmo objetivo — confiança — mas chegam lá de formas diferentes.
Testes são excelentes para achar erros concretos: um off-by-one, um caso de borda faltante, uma regressão. Mas uma suíte de testes só pode amostrar o espaço de entradas. Mesmo “100% de cobertura” não significa “todos os comportamentos checados”; geralmente significa “todas as linhas executadas.”
Raciocínio no estilo prova (especialmente ao estilo Hoare) parte de uma especificação e pergunta: se essas precondições se mantêm, o código sempre estabelece as postcondições? Quando bem feito, você não apenas encontra um bug — pode eliminar uma categoria inteira de bugs (como “acessos a arrays ficam nos limites” ou “o laço nunca quebra a propriedade de partição”).
Uma especificação clara é um gerador de testes.
Se sua postcondição diz “a saída está ordenada e é uma permutação da entrada”, você automaticamente obtém ideias de testes:
A spec diz o que “correto” significa, e os testes checam se a realidade bate com isso.
Testes baseados em propriedades ficam entre provas e exemplos. Em vez de escolher alguns casos à mão, você declara propriedades e deixa uma ferramenta gerar muitas entradas.
Para ordenação, duas propriedades simples ajudam bastante:
Essas propriedades são essencialmente postcondições escritas como checagens executáveis.
Uma rotina leve que escala:
Se quiser institucionalizar isso, coloque “spec + notas de raciocínio + testes” como parte do template de PR ou da checklist de revisão de código (veja também /blog/code-review-checklist).
Se você usa um fluxo de trabalho de geração de código por chat (vibe-coding), a mesma disciplina se aplica — talvez mais: no Koder.ai, por exemplo, você pode começar no Planning Mode para fixar precondições/postcondições antes de gerar código, e então iterar com snapshots e rollback enquanto adiciona testes baseados em propriedades. A ferramenta acelera a implementação, mas é a spec que impede que “rápido” vire “frágil”.
Corretude não é só “o programa retorna o valor certo”. Pensamento de segurança faz uma pergunta diferente: quais resultados são inaceitáveis, e como impedimos que eles aconteçam — mesmo quando o código é forçado, mal utilizado ou parcialmente falho? Na prática, segurança é corretude com uma hierarquia de prioridades: algumas falhas são apenas incômodas, outras podem causar perda financeira, vazamento de privacidade ou dano físico.
Um bug é um defeito no código ou no design. Um risco (hazard) é uma situação que pode levar a um resultado inaceitável. Um bug pode ser inofensivo num contexto e perigoso em outro.
Exemplo: um erro off-by-one em uma galeria de fotos pode rotular mal uma imagem; o mesmo erro em um calculador de dosagem de medicamentos pode ferir um paciente. Pensamento de segurança força você a conectar o comportamento do código às consequências, não apenas à “conformidade com a spec”.
Você não precisa de métodos formais pesados para obter ganhos imediatos de segurança. Equipes podem adotar práticas pequenas e repetíveis:
Essas técnicas se encaixam naturalmente com raciocínio ao estilo Hoare: você torna precondições explícitas (quais entradas são aceitáveis) e assegura que as postcondições incluam propriedades de segurança (o que nunca deve acontecer).
Checagens orientadas à segurança custam — CPU, complexidade ou rejeições ocasionais.
Pensamento de segurança é menos sobre provar elegância e mais sobre prevenir modos de falha que você não pode tolerar.
Revisões de código são onde o pensamento de corretude paga mais rápido, porque você pode detectar suposições ausentes muito antes de bugs chegarem à produção. O movimento central de Hoare — declarar o que deve ser verdade antes e o que será verdade depois — se traduz bem em perguntas de revisão.
Ao ler uma mudança, tente enquadrar cada função chave como uma pequena promessa:
Um hábito simples para revisores: se você não consegue dizer a pre/post em uma frase, o código provavelmente precisa de estrutura mais clara.
Para funções arriscadas ou centrais, adicione um pequeno comentário de contrato acima da assinatura. Mantenha-o concreto: entradas, saídas, efeitos colaterais e erros.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Esses comentários não são provas formais, mas dão aos revisores algo preciso para checar.
Seja extra explícito ao revisar código que lida com:
Se a mudança tocar qualquer um desses, pergunte: “Quais são as precondições, e onde elas são aplicadas?” e “Que garantias oferecemos mesmo quando algo falha?”
Raciocínio formal não precisa significar transformar toda sua base de código em um artigo matemático. O objetivo é gastar certeza extra onde vale a pena: lugares onde “parece bem nos testes” não é suficiente.
São adequados quando você tem um módulo pequeno e crítico do qual tudo depende (autenticação, regras de pagamento, permissões, intertravamentos de segurança), ou um algoritmo complicado onde erros off-by-one se escondem por meses (parsers, escalonadores, cache/evicção, código do tipo partição, transformações de dados com muitas fronteiras).
Uma regra útil: se um bug pode causar dano real, grande perda financeira ou corrupção silenciosa de dados, você quer mais que revisão comum + testes.
Você pode escolher desde “leve” até “pesado”, e frequentemente o melhor resultado vem de combiná-las:
Decida a profundidade da formalidade pesando:
Na prática, você pode tratar “formalidade” como algo incremental: comece com contratos e invariantes explícitos, depois deixe automação manter isso. Para equipes que constroem rápido com Koder.ai — onde gerar um front-end React, um backend Go e um schema Postgres pode ocorrer num ciclo curto — snapshots/rollback e exportação de código facilitam iterar rápido mantendo contratos via testes e análise estática na CI.
Use isto como uma porta de entrada “devemos formalizar mais?” no planejamento ou na revisão de código:
Leituras adicionais: design-by-contract, testes baseados em propriedades, model checking para máquinas de estado, analisadores estáticos para sua linguagem e material introdutório sobre assistentes de prova e especificação formal.
Corretude significa que o programa satisfaz uma especificação acordada: para toda entrada permitida e estado relevante do sistema, ele produz as saídas e efeitos colaterais exigidos (e trata erros conforme prometido). “Parece funcionar” normalmente quer dizer que você checou só alguns exemplos, não todo o espaço de entradas nem as condições de contorno delicadas.
Requisitos são o objetivo de negócio em linguagem natural (por exemplo, “ordenar a lista para exibição”). Uma especificação é a promessa precisa e verificável (por exemplo, “retorna uma nova lista ordenada em ordem ascendente, com a mesma multiconjunto de elementos, e sem modificar a entrada”). A implementação é o código. Bugs frequentemente aparecem quando equipes pulam a especificação e vão direto dos requisitos para o código.
Partial correctness (corretude parcial): se o código retorna, o resultado está correto. Total correctness (corretude total): o código retorna e o resultado está correto — a terminação faz parte da garantia.
Na prática, corretude total importa sempre que “ficar preso para sempre” é uma falha visível ao usuário, um vazamento de recursos ou um risco de segurança.
Uma tripla de Hoare {P} C {Q} lê-se como um contrato:
P (precondição): o que deve ser verdade antes de executar CPrecondições são o que o código precisa (por exemplo, “índices estão no intervalo”, “elementos são comparáveis”, “o lock está adquirido”). Se uma precondição pode ser violada pelos chamadores, então ou:
Caso contrário, suas postcondições viram desejos, não garantias.
Um invariante de laço é uma afirmação que é verdadeira antes do laço começar, permanece verdadeira após cada iteração e ainda é verdadeira quando o laço termina. Modelos úteis incluem:
0 <= i <= n)Se você não consegue articular um invariante, é um sinal de que o laço está fazendo coisas demais ou os limites estão confusos.
Normalmente você nomeia uma medida (variant) que diminui a cada iteração e não pode diminuir indefinidamente, por exemplo:
n - i diminui em 1Se não conseguir encontrar uma medida que diminua, pode haver risco real de não-terminação (especialmente com duplicatas ou ponteiros que empacaram).
Na Quicksort, a partição é a rotina pequena da qual tudo depende. Se a partição estiver levemente errada, você pode obter:
Por isso é útil declarar explicitamente o contrato da partição: o que deve ser verdade à esquerda, à direita, e que os elementos apenas foram rearranjados (uma permutação).
Duplicatas e o tratamento de “igual ao pivô” são pontos comuns de falha. Regras práticas:
i/j fiquem parados)Se duplicatas forem comuns, considere partição em três vias para reduzir bugs e profundidade de recursão.
Testes detectam erros concretos; raciocínio “estilo prova” pode eliminar categorias inteiras de bugs (segurança de limites, preservação de invariantes, terminação). Um fluxo prático é:
Para ordenação, duas propriedades de alto valor são:
CQ (postcondição): o que será verdade depois que C terminar, assumindo que P era verdadeiroVocê não precisa escrever a notação no código — usar essa estrutura em revisões (“assunções entrando, garantias saindo”) é a vantagem prática.