A lacuna entre especificação e código é onde moram os bugs

Volta e meia surge nos círculos de teoria de linguagens de programação a afirmação de que 'uma especificação suficientemente detalhada é indistinguível do código'. A implicação é provocativa: a linha entre descrever o que um programa deveria fazer e de fato fazê-lo é bem mais fina do que imaginamos. Se a sua especificação for precisa a ponto de eliminar toda ambiguidade, você basicamente já escreveu o programa.

Isso não é só filosofia. Tem implicações práticas para a forma como construímos software, para o papel que as especificações desempenham e para o motivo de a maioria dos bugs não ser erro de codificação, e sim lacuna de especificação. Entender onde a especificação termina e a implementação começa muda a forma como você pensa sobre testes, tipos e corretude.

De onde vêm a maioria dos bugs

Pergunte a um desenvolvedor de onde vêm os bugs e ele provavelmente dirá 'do código'. Mas estudos e mais estudos sobre defeitos de software mostram outra coisa: a maioria dos bugs se origina na lacuna entre a intenção e a implementação. O código faz exatamente o que o desenvolvedor mandou fazer. Só que o desenvolvedor mandou fazer a coisa errada porque a especificação, formal ou informal, era ambígua, incompleta ou mal interpretada.

Um exemplo clássico: a especificação diz 'o sistema deve tratar requisições concorrentes'. O que significa 'tratar'? Processar em ordem? Processar ao mesmo tempo? Enfileirar se forem muitas? Quantas são 'muitas'? O que acontece com as requisições que chegam enquanto a fila está cheia? Essas perguntas não são detalhes de implementação, são lacunas de especificação. E cada pergunta sem resposta é um bug em potencial, porque o desenvolvedor vai respondê-la implicitamente na implementação, e a resposta dele pode não bater com o que os usuários ou outros desenvolvedores esperam.

O espectro de precisão de uma especificação

Especificações existem num espectro que vai do informal ao formal.

• Linguagem natural. 'O sistema de login deve ser seguro e fácil de usar.' Isso mal é uma especificação, é um desejo. Cada palavra é ambígua. O que conta como 'seguro'? O que conta como 'fácil de usar'? São julgamentos de valor disfarçados de requisitos.
• Linguagem natural estruturada. 'Quando um usuário digitar a senha incorreta três vezes em 10 minutos, bloquear a conta por 30 minutos.' Mais preciso, mas ainda ambíguo. Uma submissão vazia conta como 'senha incorreta'? As três tentativas precisam ser consecutivas? A janela de 10 minutos é deslizante ou fixa?
• Assinaturas de tipo. authenticate(username: string, password: string) -> Result<User, AuthError>. Isso especifica com precisão a interface da função, mas não diz nada sobre o comportamento. Você conhece o formato do que entra e do que sai, mas não a relação entre eles.
• Especificações baseadas em propriedades. 'Para todo par usuário-senha válido no banco, authenticate retorna Ok(user) onde user.username == username.' Isso restringe o comportamento com mais precisão, usando quantificadores lógicos.
• Especificação formal. Um modelo matemático completo do comportamento do sistema: cada estado, cada transição, cada invariante. Nesse nível, a especificação e a implementação são quase a mesma coisa.

Quanto mais você se aproxima da especificação formal, menos espaço sobra para ambiguidade e, portanto, para bugs. Mas cada passo exige mais esforço e habilidades mais especializadas. A pergunta prática é: até que ponto, nesse espectro, vale a pena ir em um determinado projeto?

Tipos como especificações leves

Sistemas de tipos são a forma de especificação mais adotada na programação do dia a dia. Eles não descrevem comportamento, mas o restringem. Uma função que retorna Option<User> em vez de User especifica que pode não encontrar um usuário, e o compilador obriga cada chamador a tratar essa possibilidade.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

Linguagens como Rust, Haskell e TypeScript mostram como sistemas de tipos expressivos reduzem a lacuna de especificação sem exigir treinamento em métodos formais. Tipos algébricos, restrições genéricas e pattern matching exaustivo juntos especificam bastante comportamento no nível dos tipos, e o compilador verifica tudo automaticamente.

A ideia central: cada anotação de tipo é uma especificação que é verificada automaticamente. Cada comportamento que você consegue codificar no sistema de tipos é uma classe de bugs que você nunca vai ter.

Property-based testing: especificando comportamento

Testes unitários são especificações baseadas em exemplos: 'dada esta entrada específica, espere esta saída específica'. Eles são úteis, mas inerentemente incompletos, porque você só testa os casos em que pensou. O property-based testing inverte essa lógica: você especifica propriedades que devem valer para todas as entradas, e o framework de testes gera entradas aleatórias para encontrar violações.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

As três propriedades desse teste não apenas testam a ordenação, elas a definem. Qualquer função que satisfaça as três propriedades é, por definição, uma ordenação correta. Essa é a ideia de 'especificação como código' na sua forma mais prática: escreva propriedades que definem o comportamento correto e deixe o framework de testes verificar se a sua implementação as satisfaz.

TLA+ e model checking

Para sistemas em que bugs custam caro, como sistemas distribuídos, plataformas financeiras e infraestrutura crítica, ferramentas de especificação formal como o TLA+ oferecem garantias mais fortes. O TLA+ (Temporal Logic of Actions) permite especificar o comportamento de um sistema como uma máquina de estados e depois fazer model checking: explorar exaustivamente todas as execuções possíveis para verificar se os invariantes se mantêm.

A Amazon usa TLA+ para verificar algoritmos do S3, do DynamoDB e de outros serviços críticos da AWS. Eles já relataram publicamente bugs que seriam praticamente impossíveis de achar só com testes, bugs que aparecem apenas em intercalações específicas de operações concorrentes, que ocorrem uma vez em milhões de execuções.

A especificação em TLA+ de um protocolo de consenso como o Raft costuma ter algumas centenas de linhas. Ela descreve cada transição de estado legal, cada invariante (por exemplo, 'no máximo um líder por mandato') e cada propriedade de segurança. O model checker então explora bilhões de caminhos de execução possíveis, verificando que nenhum deles viola algum invariante. Isso é especificação genuinamente próxima de código, precisa o suficiente para que você conseguisse traduzi-la mecanicamente para uma implementação.

Design by Contract

O Design by Contract (DbC), de Bertrand Meyer, fica num meio-termo bem prático. Cada função especifica pré-condições (o que precisa ser verdade antes de a função ser chamada), pós-condições (o que a função garante ao retornar) e invariantes (o que precisa ser sempre verdade para o objeto). Esses contratos são verificados em tempo de execução durante o desenvolvimento e podem ser desativados em produção por performance.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

A pós-condição de conservação, de que o total de dinheiro antes e depois da transferência é o mesmo, é o tipo de invariante que pega bugs que testes unitários raramente cobrem. Ela especifica uma propriedade fundamental do sistema (dinheiro não é criado nem destruído) que qualquer implementação correta precisa satisfazer.

Recomendações práticas

Especificação formal completa não é prática para a maioria dos softwares. Mas você pode reduzir bastante a lacuna de especificação com técnicas que cabem num fluxo de desenvolvimento normal.

1. Use o sistema de tipos com agressividade. Codifique restrições como tipos sempre que possível. Prefira NonEmptyList a List quando a lista não puder ser vazia. Use wrappers newtype para diferenciar UserId de OrderId, mesmo que ambos sejam strings. Toda restrição codificada em tipos é uma restrição que o compilador verifica de graça.
2. Escreva testes baseados em propriedades para a lógica central. Identifique os invariantes que o seu sistema deve manter e expresse-os como property tests. Algumas poucas propriedades bem escolhidas pegam bugs que milhares de testes baseados em exemplos deixam passar.
3. Especifique as fronteiras. As especificações mais importantes ficam nas fronteiras do sistema: contratos de API, schemas de banco de dados, formatos de mensagem. Use OpenAPI, Protocol Buffers ou JSON Schema para torná-las verificáveis por máquina.
4. Use TLA+ ou Alloy em sistemas concorrentes críticos. Se você está projetando um algoritmo de consenso, um lock distribuído ou um sistema de transações financeiras, o custo da especificação formal é pequeno perto do custo de bugs de corretude sutis em produção.
5. Escreva a especificação antes dos testes. Se você não consegue afirmar com precisão como é o comportamento correto, não consegue verificá-lo. Gastar 30 minutos escrevendo uma especificação clara do que uma função deve fazer (todos os casos, incluindo as bordas) costuma revelar problemas de design antes de você escrever uma única linha de código.

A afirmação de que 'uma especificação suficientemente detalhada é código' não está bem certa. É mais preciso dizer que uma especificação suficientemente detalhada elimina o espaço para bugs. A lacuna entre especificação e implementação é onde mora a ambiguidade, e é na ambiguidade que os bugs se reproduzem. Toda técnica que reduz essa lacuna, como tipos, propriedades, contratos e métodos formais, torna o software mais correto. Não porque impeça erros de codificação, mas porque impede os erros de especificação de que os erros de codificação geralmente surgem.