Vale reescrever Fortran em Rust ou criar uma camada?

Um núcleo Fortran que produz resultados confiáveis há vinte anos não vira código ruim porque o aplicativo ao redor ficou difícil de manter. Se o núcleo tem uma interface estreita, builds reproduzíveis e alguém que ainda consegue diagnosticá-lo, encapsulá-lo atrás de uma interface moderna costuma ser a decisão mais barata e segura. A linguagem de origem, sozinha, não é motivo para reescrever uma matemática que funciona.

A decisão muda quando o núcleo antigo passa a controlar a implantação, bloquear opções de hardware, esconder estado mutável ou exigir conhecimentos que a organização já não consegue oferecer. Nesse ponto, preservá-lo tem um preço recorrente. Uma migração para Rust pode custar menos do que outro ciclo de compiladores especiais, hosts obsoletos, releases manuais e incidentes que apenas um engenheiro aposentado entende. O difícil é comparar esses custos sem tratar idade como defeito ou correção no passado como prova de operação futura.

Separe o valor do algoritmo do custo do seu contêiner

Um algoritmo comprovado e sua implementação em Fortran são ativos relacionados, mas não são o mesmo ativo. As equações, os coeficientes, as regras de convergência e o comportamento aceito nos limites podem merecer preservação mesmo quando o sistema de build e as premissas de execução não merecem.

Equipes costumam chamar um núcleo de "comprovado" quando querem dizer que a produção depende dele há anos. Esse histórico importa, mas responde a apenas uma pergunta: o sistema completo gerou resultados aceitáveis para as entradas que realmente recebeu? Ele não demonstra que o código é portátil, livre de comportamento indefinido, seguro sob concorrência ou compreensível depois que o responsável atual sair. Uma vida longa pode até esconder dependências, pois ninguém recompilou o núcleo recentemente em uma máquina limpa.

Registre o que torna o núcleo digno de preservação antes de escolher um tratamento. O inventário útil é concreto:

• O modelo matemático e a versão aceita pelo negócio
• Os intervalos de entrada vistos em produção, incluindo casos inválidos e degenerados
• A precisão exigida, o comportamento de arredondamento e as tolerâncias de convergência
• Os limites de tempo e memória que afetam um lote ou uma requisição reais
• As opções do compilador, bibliotecas vinculadas, arquivos de dados e ordem de inicialização

Esse inventário expõe uma distinção importante. Paridade numérica significa que a nova execução permanece dentro de uma tolerância acordada. Paridade de comportamento também cobre erros, avisos, contagem de iterações, ordem da saída, tratamento de NaN, timeouts e efeitos colaterais. Uma migração pode cumprir a primeira definição e quebrar o aplicativo pela segunda. Uma camada pode preservar ambas, mas somente se sua interface não mudar a representação ou o ciclo de vida em silêncio.

A idade do código-fonte deve ficar perto do fim do registro da decisão. As obrigações observáveis ficam no início. Se ninguém consegue descrevê-las, nem o encapsulamento nem a reescrita estão prontos. Primeiro é preciso recuperar o contrato a partir do código e das evidências de produção.

Uma interface estreita e estável favorece o encapsulamento

Encapsule o núcleo quando seus chamadores puderem descrevê-lo como um pequeno conjunto de operações determinísticas com entradas e saídas numéricas comuns. Um bom candidato se parece mais com uma biblioteca do que com um aplicativo: inicializa tabelas imutáveis, recebe arrays e opções escalares, calcula e devolve resultados e status.

Conte os pontos da interface, não as linhas de Fortran. Um solver de 300 mil linhas exposto por seis operações estáveis pode ser mais fácil de conter do que uma rotina de 6 mil linhas que lê arquivos globais, altera blocos COMMON, grava relatórios e chama de volta uma interface de usuário. O segundo núcleo tem uma superfície de comportamento maior, embora o código-fonte seja menor.

Uma camada é atraente quando todas estas condições são atendidas:

• Um compilador com suporte consegue reproduzir o binário nos hosts previstos
• O núcleo tem testes ou casos gravados com saídas confiáveis
• As chamadas não dependem de estado oculto do processo, ou esse estado pode ser isolado
• Os custos de conversão de dados são pequenos diante do tempo de cálculo
• Correções de segurança e diagnósticos chegam à interface sem alterar a matemática

A camada deve cuidar de validação, limites de memória, informações de versão, telemetria e tradução entre os tipos do aplicativo e os tipos Fortran. Ela não deve fingir que corrige o comportamento numérico. Manter essa divisão clara permite que engenheiros de aplicação melhorem a operação sem mudar por acidente o contrato dos resultados.

Há também um teste organizacional útil: um novo engenheiro consegue recompilar a biblioteca, executar seus casos e localizar uma chamada com falha sem perguntar ao autor original? Se consegue, manter o núcleo é uma dependência controlada. Caso contrário, a camada talvez apenas esconda um programa órfão. Documentação sozinha não resolve isso. O build e o diagnóstico precisam funcionar em uma máquina vazia.

Use a ABI de C como uma junção pequena e simples

Fortran e Rust podem compartilhar um limite confiável pela interface binária de C, desde que o lado Fortran use ISO_C_BINDING em vez de convenções de símbolos específicas do compilador. A junção deve expor tipos numéricos de largura fixa, comprimentos de arrays explícitos, buffers planos e códigos inteiros de status.

Este ponto de entrada Fortran deixa a disposição dos dados visível:

module kernel_api
  use, intrinsic :: iso_c_binding
  implicit none
contains
  subroutine evaluate(n, x, scale, y, status) bind(C, name="kernel_evaluate")
    integer(c_int), value :: n
    real(c_double), intent(in) :: x(n)
    real(c_double), value :: scale
    real(c_double), intent(out) :: y(n)
    integer(c_int), intent(out) :: status

    if (n < 1 .or. scale <= 0.0_c_double) then
      status = 1_c_int
      return
    end if

    call legacy_evaluate(n, x, scale, y)
    status = 0_c_int
  end subroutine evaluate
end module kernel_api

O lado Rust mantém a operação unsafe em um módulo pequeno e apresenta uma API de slices verificada ao restante do aplicativo:

unsafe extern "C" {
    fn kernel_evaluate(
        n: i32,
        x: *const f64,
        scale: f64,
        y: *mut f64,
        status: *mut i32,
    );
}

pub fn evaluate(x: &[f64], scale: f64) -> Result<Vec<f64>, KernelError> {
    let n = i32::try_from(x.len()).map_err(|_| KernelError::InputTooLarge)?;
    if x.is_empty() || !scale.is_finite() || scale <= 0.0 {
        return Err(KernelError::InvalidInput);
    }

    let mut y = vec![0.0_f64; x.len()];
    let mut status = 0_i32;
    unsafe {
        kernel_evaluate(n, x.as_ptr(), scale, y.as_mut_ptr(), &mut status);
    }

    match status {
        0 => Ok(y),
        code => Err(KernelError::Fortran(code)),
    }
}

Esse código é pouco impressionante de propósito. Isso é uma qualidade na fronteira entre linguagens. O Rust Nomicon descreve chamadas de funções externas como unsafe porque o compilador não pode verificar o contrato da outra linguagem. Mantenha o bloco unsafe pequeno o bastante para ser auditado e deixe cada pré-condição visível antes da chamada.

O manual de interoperabilidade do GNU Fortran explica como procedimentos e tipos interoperáveis são mapeados por BIND(C) e ISO_C_BINDING. Siga esse mecanismo em vez de depender da decoração de nomes habitual de um compilador. Um símbolo exportado encontrado com uma ferramenta de inspeção binária comprova o build atual, mas não oferece uma interface estável para o compilador de amanhã.

Não envie structs de Rust, tipos derivados de Fortran, arrays alocáveis ou strings nativas das linguagens pela primeira versão dessa junção. Achate os dados. Para matrizes, documente dimensões, dimensão principal e ordem de armazenamento. Para texto, passe um buffer de bytes com comprimento e regra de codificação explícitos. Representações simples evitam ambiguidades caras.

Estado oculto faz camadas falharem

Uma camada falha quando faz um programa com estado parecer uma função pura sem controlar esse estado. Variáveis SAVE, blocos COMMON, arrays de trabalho em cache, variáveis de ambiente, números de unidade, arquivos do diretório de trabalho e o modo de ponto flutuante podem mudar o resultado de uma chamada aparentemente idêntica.

A concorrência costuma revelar primeiro o engano. Duas requisições web entram na camada ao mesmo tempo, ambas alteram a mesma área de trabalho salva e uma resposta contém valores derivados da entrada da outra. Um mutex pode restaurar a correção, mas também serializa a vazão. O isolamento por processos pode preservar o paralelismo ao custo de memória e tempo de inicialização. Nenhuma opção é automaticamente errada, mas ambas precisam aparecer no modelo de capacidade.

A inicialização é outra fonte comum de falhas. O executável original pode ler coeficientes, definir uma semente aleatória ou chamar uma rotina de preparação antes do caminho numérico. A extração de uma biblioteca que exporta apenas a sub-rotina final pode retornar números plausíveis a partir de estado não inicializado ou padrão. Esses números são mais perigosos que uma queda, pois o monitoramento pode aceitá-los.

Mapeie o ciclo de vida completo da chamada:

1. Inicie um processo novo e registre cada arquivo, valor de ambiente e biblioteca carregados.
2. Acompanhe a inicialização até que a primeira operação numérica possa executar.
3. Chame o mesmo caso duas vezes e compare todas as saídas e valores de status.
4. Intercale dois casos diferentes e repita-os depois em processos separados.
5. Force uma entrada inválida, uma falha de alocação quando for viável e a não convergência.

Essa sequência mostra se o núcleo pode viver dentro de um serviço com várias threads, precisa de uma única fila de workers ou deve ficar em processos isolados. Ela também identifica caminhos de erro que encerram o processo com STOP, escrevem na saída padrão ou deixam resultados parciais. Uma camada não pode traduzir um erro depois que o runtime Fortran encerrou o processo hospedeiro.

A disposição dos arrays merece uma verificação própria. Fortran armazena arrays por coluna; bibliotecas Rust muitas vezes presumem ordem por linha. Uma matriz copiada pode parecer correta nas dimensões e ainda representar sua transposta ou um passo de memória errado. Teste uma matriz não quadrada com valores exclusivos, pois casos quadrados ou simétricos escondem o engano. Se as cópias de conversão dominarem o tempo da chamada, altere a interface para aceitar a disposição nativa do núcleo em vez de pagar por duas passagens completas na memória.

Comprove a paridade com evidências parecidas com produção

Paridade exige uma comparação executável, não uma revisão de código nem algumas saídas de referência. Execute os caminhos antigo e candidato com as mesmas entradas gravadas, capture todos os resultados observáveis e classifique cada diferença.

Comece com tráfego de produção ou registros de lotes depois de remover dados que não devem existir no ambiente de teste. Os registros carregam combinações que testes sintéticos não encontram: grupos vazios ao lado de grupos grandes, ordenação incomum, sinalizadores antigos, valores perto de um limite e novas tentativas após trabalho parcial. Acrescente casos construídos para limites e estresse numérico, mas não permita que substituam as formas reais de operação.

Um verificador útil emite um registro como este para cada chamada:

{
  "case_id": "settlement-004812",
  "operation": "evaluate",
  "input_digest": "sha256:...",
  "old": {"status": 0, "iterations": 7, "output": [1.25, 3.5]},
  "candidate": {"status": 0, "iterations": 7, "output": [1.25, 3.5]},
  "comparison": {"max_abs": 0.0, "max_rel": 0.0, "accepted": true}
}

Não escolha um epsilon global apenas por conveniência. A tolerância absoluta funciona perto de zero; a relativa funciona conforme as magnitudes crescem; algumas saídas exigem limites baseados em unidades; inteiros exatos e valores de status precisam de igualdade exata. NaNs exigem uma regra explícita porque a igualdade comum os trata de modo diferente dos valores finitos. O zero com sinal pode importar quando operações posteriores inspecionam esse sinal.

Compare falhas com o mesmo cuidado dedicado aos cálculos bem-sucedidos. Se o caminho antigo informa não convergência após 40 iterações e o novo retorna a última estimativa como sucesso, os arrays podem estar próximos mesmo com um contrato diferente. Se a ordem de saída não está especificada no código-fonte, mas o código seguinte depende dela há anos, o comportamento em produção torna essa ordem uma obrigação da migração até que os chamadores mudem.

Mantenha o verificador depois da entrega. Ele vira a proteção para atualizações do compilador, mudanças nas opções de otimização, substituições de bibliotecas e trabalhos posteriores em Rust. A CodeHero usa esse tipo de verificador de paridade com tráfego de produção gravado enquanto moderniza a arquitetura, pois uma suíte de testes unitários aprovada não prova sozinha que um sistema legado mantém o comportamento nos limites.

Reescreva quando os custos de propriedade forem recorrentes

Migre o núcleo quando mantê-lo gerar um imposto operacional recorrente que uma camada não consegue remover. Os motivos mais fortes envolvem propriedade e implantação, não preferência por linguagem.

Uma migração merece avaliação séria quando o compilador Fortran aprovado não oferece suporte ao ambiente de destino, o build depende de bibliotecas abandonadas ou cada release exige um host que a organização já quer aposentar. O mesmo vale quando o diagnóstico em produção termina em um binário opaco e as falhas não podem ser relacionadas a entradas, fases ou uso de recursos.

A equipe disponível importa, mas "não contratamos desenvolvedores Fortran" é um argumento fraco sozinho. Um núcleo estável e encapsulado pode exigir pouco trabalho nessa linguagem. Meça a demanda real: com que frequência o algoritmo muda, quantos incidentes exigem diagnóstico no código-fonte, quem revisa atualizações do compilador e o que acontece quando o responsável atual está indisponível? Migrar apenas para combinar com a linguagem majoritária pode consumir um orçamento grande sem reduzir essas obrigações.

Mudanças frequentes fortalecem o caso. Se o trabalho no produto adiciona termos ao modelo, altera regras de convergência ou precisa que o núcleo participe do cancelamento de requisições e de erros estruturados, cada mudança atravessa a junção. A camada passa a acumular políticas que pertencem ao cálculo. Rust oferece propriedade direta da memória, tipos de resultado explícitos, paralelismo controlado e ferramentas que mais integrantes da equipe de aplicação conseguem operar.

Existe também um argumento de segurança e isolamento. Se o núcleo consome arquivos não confiáveis, faz indexação sem verificação ou roda no mesmo processo de um serviço exposto, a contenção pode ser obrigatória antes mesmo da migração. Execute-o em um processo worker restrito com limites de entrada enquanto a reescrita avança. Rust reduz muitos erros de memória no código reescrito, mas não prova a matemática, não impede esgotamento de recursos nem torna seguras as bibliotecas externas inseguras.

Um registro de decisão útil converte problemas recorrentes em esforço anual de engenharia e custo de infraestrutura. Inclua licenças do compilador, hosts especiais de build, trabalho de release, dependência em incidentes, capacidade ociosa causada pela serialização e mudanças de plataforma bloqueadas. Não invente um valor monetário para a "modernidade". Dê valor ao trabalho que a organização realmente executa.

As configurações do compilador fazem parte do contrato

Um comando do compilador faz parte do código-fonte efetivo do núcleo. Opções de otimização, ajustes de ponto flutuante, arquitetura de destino, bibliotecas matemáticas vinculadas e até a ordem de link podem mudar resultados numéricos ou expor premissas que um build antigo tolerava por acaso.

Recupere o build exato antes de avaliar uma camada ou migração. Guarde a identidade e a versão do compilador, todas as opções de compilação e link, definições do pré-processador, versões de bibliotecas e variáveis de ambiente usadas. Capture os comandos na ferramenta de build em vez de copiar um comentário de um documento operacional antigo. Depois, recompile em um ambiente limpo e compare os casos de referência. Se um build limpo já for diferente, a equipe tem um problema de reprodutibilidade antes de iniciar a migração.

A otimização agressiva de ponto flutuante exige atenção especial. Com opções matemáticas permissivas, um compilador pode reagrupar operações, fundir uma multiplicação e uma adição, tratar NaNs como impossíveis ou supor que o sinal de zero não tem significado. Essas transformações podem melhorar a velocidade e mudar a convergência perto de um limite. A pergunta não é se uma opção segue um padrão estrito em abstrato. Pergunte se o contrato de produção permite a mudança e comprove a resposta com o verificador.

Bibliotecas numéricas externas também pertencem ao registro. Uma chamada chamada DGEMM pode manter a mesma interface enquanto outra implementação de BLAS muda a ordem da redução, o uso de threads, a seleção de CPU e o desempenho. Isso costuma ser aceitável dentro de uma tolerância bem definida, mas pode alterar o comportamento de um solver no limite ou sobrecarregar um serviço cuja camada externa também cria threads. Registre a implementação e as configurações de threads da biblioteca com cada benchmark.

Crie um manifesto de build ao lado de cada artefato candidato. Ele pode ser simples:

kernel_version=2026.08
compiler=gfortran
compiler_version=<captured from build>
compile_flags=<captured from build>
blas_implementation=<name and version>
target_cpu=<declared target>
source_digest=<repository revision>
test_corpus=<immutable corpus revision>

Os sinais de menor e maior marcam campos a preencher, não uma autorização para deixar os dados desconhecidos. Faça o build gerar esse manifesto automaticamente e exponha-o em uma operação de versão ou no log de inicialização. Quando uma saída mudar depois da implantação, os operadores poderão saber se houve mudança no código, compilador, biblioteca ou conjunto de entradas.

No encapsulamento, essa disciplina transforma o binário Fortran em um componente controlado, em vez de um arquivo inexplicado copiado entre servidores. Na migração, ela apresenta aos engenheiros Rust o comportamento real que precisam igualar. Builds Rust exigem o mesmo tratamento: fixe versões de dependências, registre a cadeia do compilador, declare recursos da CPU de destino e mantenha as opções de desempenho separadas das opções de paridade até medir seus efeitos.

Evite transformar igualdade bit a bit em objetivo universal. Ela pode ser exigida para alguns registros regulados ou checkpoints binários, mas também pode congelar um caminho de compilador e hardware por tempo indeterminado. A maioria dos sistemas numéricos precisa de tolerâncias com sentido científico ou financeiro, além de igualdade exata nas decisões discretas. Documente a categoria de cada saída. Um resultado booleano de elegibilidade não pode desviar por um epsilon, ainda que venha de cálculos de ponto flutuante.

Uma armadilha final é comparar um build antigo e conservador com um candidato configurado com todas as otimizações disponíveis e depois atribuir o resultado à linguagem. Execute uma matriz que separe implementação e configurações: Fortran de referência, Fortran otimizado, Rust conservador e Rust otimizado. Essa comparação mostra se a economia proposta vem da migração, de uma atualização do compilador ou da aceitação de um contrato numérico diferente.

O custo do hardware pode descartar uma camada correta

Um núcleo encapsulado pode preservar os resultados perfeitamente e ainda virar a opção cara quando seu modelo de execução impede o uso eficiente do hardware disponível. Meça a carga completa no hardware que você pretende operar, incluindo conversão de dados, limites entre processos, movimento de memória e filas.

Não presuma que Rust será mais rápido. Compiladores Fortran maduros geram código numérico excelente, e núcleos estabelecidos talvez já chamem rotinas BLAS ou LAPACK otimizadas. Uma migração literal pode perder vetorização, alocar com mais frequência ou trocar uma chamada de biblioteca otimizada por um laço comum. A escolha da linguagem não elimina a largura de banda da memória nem a complexidade do algoritmo.

A pressão econômica costuma aparecer em outro lugar. O núcleo pode estar compilado apenas para uma arquitetura antiga, depender de um runtime do fornecedor que limita a implantação ou serializar o trabalho por meio de estado global. Ele pode copiar arrays grandes várias vezes para se adaptar ao limite de um novo serviço. Instâncias de nuvem ficam subutilizadas enquanto requisições esperam atrás de uma única via de cálculo. Esses custos de sistema são mensuráveis e podem justificar uma migração, mesmo que uma chamada Fortran isolada continue rápida.

Meça distribuições representativas, não um único caso favorável. Registre no mínimo a vazão, a latência na cauda, o pico de memória residente, os bytes copiados na interface e o tempo gasto esperando a região serializada. Execute casos quentes e frios quando a inicialização for relevante. Fixe as versões e opções do compilador no resultado para que outro engenheiro consiga reproduzi-lo.

Depois, teste as alternativas mais baratas à reescrita. Remover uma transposição desnecessária, manter um pool de processos worker, atualizar o compilador ou trocar uma interface de arquivos por um buffer na memória pode recuperar capacidade suficiente. Se recuperar, a camada ganhou mais um período de serviço. Se o núcleo ainda bloquear a arquitetura escolhida ou um caminho de acelerador, a migração recebe uma obrigação concreta de desempenho em vez de uma promessa vaga de ser mais rápida.

Uma migração para Rust deve preservar comportamento, não sintaxe

Uma boa migração traduz o modelo de cálculo e depois lhe dá um projeto que engenheiros Rust conseguem manter. A transliteração preserva o fluxo de controle antigo, arrays globais, valores sentinela e hábitos de indexação enquanto acrescenta conflitos com o borrow checker. O resultado fica mais difícil de revisar do que qualquer um dos originais.

Congele o build de referência antes de editar. Dê a ele opções de compilador reproduzíveis, dados de teste imutáveis e uma invocação legível por máquina. A referência não precisa ser bonita. Precisa permanecer disponível até que a substituição sobreviva à comparação em produção.

Divida a migração por limites matemáticos observáveis pelo verificador de paridade. Boas unidades incluem pré-processamento, seleção de coeficientes, uma iteração do solver, avaliação da convergência e formatação do resultado. Migre uma unidade, chame-a pelo caminho existente quando for prático e compare valores intermediários. Isso restringe uma diferença a uma etapa, em vez de pedir aos engenheiros que examinem um solver inteiro.

Deixe as decisões numéricas explícitas em Rust. Declare se os valores são f32 ou f64, como uma conversão de inteiros trata overflow, qual ordem de redução é aceitável e se uma multiplicação e adição fundidas podem mudar o arredondamento. Primeiro preserve o algoritmo aceito. Melhore-o depois em uma mudança revisada separadamente e com evidências próprias, pois combinar migração de linguagem e revisão do modelo destrói a referência limpa.

Modele falhas como resultados tipados em vez de valores mágicos, mas mantenha o comportamento externo anterior até que os chamadores adotem deliberadamente o novo contrato. Se o caminho Fortran emite um aviso e uma estimativa utilizável, o primeiro release Rust não deve transformar esse caso em erro fatal silenciosamente. APIs melhores só ajudam quando o sistema ao redor muda com elas.

Limite Rust unsafe às fronteiras com outras linguagens e a chamadas de bibliotecas auditadas. Rust puro ainda pode entrar em panic por indexação, alocar sem um limite prático ou produzir NaNs a partir de operações válidas de ponto flutuante. Defina limites e devolva falhas na interface do serviço. Segurança de memória resolve uma classe de defeitos, não o contrato operacional.

Mantenha a decisão reversível até que as evidências a encerrem

O programa mais seguro adia a escolha irreversível enquanto melhora as duas opções. Primeiro crie um build Fortran reproduzível e um verificador de paridade. Depois coloque o núcleo existente atrás da interface que você desejaria mesmo se a implementação mudasse. Esse trabalho é necessário para uma camada confiável e continua útil para uma migração.

Execute a versão encapsulada sob carga representativa. Agora você tem evidências sobre custo de conversão, concorrência, isolamento de falhas e propriedade operacional. Se ela cumprir o objetivo do serviço e a equipe conseguir manter seu build, pare. Manter um bom Fortran é uma decisão de engenharia, não falta de ambição.

Se ela não cumprir, a mesma interface se torna o limite da substituição em Rust, e os mesmos casos gravados avaliam cada unidade migrada. Faça uma implantação com comparação em sombra quando o ambiente permitir: execute o candidato sem deixar que ele controle a resposta, registre diferenças limitadas e examine casos fora da tolerância. Proteja entradas sensíveis e limite a carga extra de cálculo. Execução em sombra é uma técnica de teste, não permissão para duplicar dados sem cuidado.

Defina critérios de saída antes que a migração ganhe impulso próprio. Eles devem cobrir paridade aceita, desempenho nos hosts previstos, comportamento em falhas, diagnósticos operacionais e remoção da dependência do runtime antigo. Defina também a janela de reversão e as evidências necessárias para aposentar a referência. Sem essas condições, equipes mantêm duas implementações por tempo indeterminado e pagam os dois custos de propriedade.

A decisão agora pode ser expressa sem ideologia. Encapsule quando o cálculo for estável, a interface estreita e a cadeia de ferramentas continuar operável. Reescreva quando as restrições recorrentes de propriedade ou hardware custarem mais do que uma migração medida e quando a organização puder comprovar a nova implementação contra a antiga. Se você ainda não consegue provar nenhuma das afirmações, use o próximo dia de engenharia no verificador, não na tradução de um laço.