Desenvolvimento de uma ferramenta de análise assintótica automatizada de programas

Abstract

Esta monografia apresenta o desenvolvimento de uma ferramenta para a automação da análise assintótica de programas, motivada pela complexidade e pela possibilidade de erros inerentes à análise manual de algoritmos. O trabalho fundamenta-se na Ciência da Computação teórica, unindo a Análise de Algoritmos à Verificação Formal com o objetivo de fornecer uma solução confiável e automatizada para o auxílio de profissionais e estudantes. Para atingir esse objetivo, foram explorados os fundamentos da Lógica de Hoare, incluindo conceitos de correção e completude, adaptando-a para a análise de custos computacionais com base nos trabalhos de Silva (2022). A metodologia proposta resultou na implementação de um Gerador de Condições de Verificação, que utiliza o algoritmo de pré-condição mais fraca de custo para traduzir especificações de programas em metas de prova rigorosas. Os resultados demonstram a viabilidade e eficácia da abordagem. A ferramenta, validada através de exemplos práticos, mostrou-se capaz de garantir a correção lógica e validar limites superiores de custo de execução, permitindo a inferência segura da complexidade assintótica a partir de custos absolutos. Assim, o estudo estabelece o núcleo prático de uma ferramenta que integra verificação formal e análise de desempenho, mitigando a necessidade de contagem manual de operações e elevando a precisão das análises.