A Verificação Formal de programas vai acabar com a necessidade de Testes?
No último post falei da verificação e corretude de programas, da lógica de Hoare e de ferramentas que apoiam o desenvolvedor/arquiteto a verificar formalmente se uma implementação está de acordo com a especificação.
Existe um artigo recente do Hoare na ACM communications de Outubro de 2009 (Retrospective: An Axiomatic Basis for Computer Programming) que é interessante para quem gosta deste tópico.
Nele, o cientista discorre sobre seus muitos anos de esforços rumo à verificação, que teve como base o uso da lógica e a definição formal das linguagens de programação. Seu objetivo era eliminar erros e, neste caso, a prova formal de programas eliminaria a necessidade de testes.
Em certo ponto ele confessa: “Em um ponto eu estava espetacularmente errado. Eu pude perceber que os programas estavam ficando maiores e eu pensei que testar poderia ser um caminho crescentemente ineficaz de remover seus erros”. Onde estava seu engano? “Eu não percebi que o sucesso dos testes é que eles testam o programador, não o programa.”...”A falha num teste pune qualquer lapso de concentração do programar e (tão importante quanto) a contagem de falhas permitem aos implementadores resistirem a pressões gerenciais para a distribuição prematura de um código não confiável.” Mais adiante: “... de fato ambos (testes e verificação formal) são valiosos e suportam mutualmente meios para acumular evidências da corretude e “serviciability” dos programas”.
Existem vários pontos que nos levam ao uso ou não de testes e/ou verificação formal:
- Custo. No estágio atual, a verificação formal ainda é cara, mas pode se justificar caso haja riscos de vida ou de perdas significativas caso falhas ocorram;
- A verificação formal não nos protege contra erros de especificação;
- Existem erros, como as vulnerabilidades de segurança, que são extremamente difíceis de testar. Neste caso, o uso da verificação formal parece ser inestimável.
Recado dado: nada de sonhar em um dia parar com testes e provas de conceito. A verificação formal será mais uma arma no nosso arsenal.
Minha experiência pessoal diz que especificar, testar e implementar são coadjuvantes. Ao testar e desenhar testes pegamos tanto erros de programação quanto de especificação; ao programar pegamos erros nos testes e na especificação; ao checar contra a especificação pegamos erros tanto nos nossos testes quanto na implementação… e, nesta luta contra erros, todas ferramentas são bem vindas.
Para terminar, uma visão dada pelo próprio Hoare: num futuro, “… eu espero que o fenômeno do erro de programação seja reduzido à insignificância: a programação de computadores será reconhecida como a mais confiável das disciplinas da engenharia e os programas de computação serão considerados os componentes mais confiáveis em qualquer sistema que os incluam”.
Um belo objetivo a ser perseguido!
Abraços
(obs.: todas traduções são minhas)