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:

1. 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;
2. A verificação formal não nos protege contra erros de especificação;
3. 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)

Comments

• Anonymous
  February 23, 2010
  Bom esse post Otavio! No último ano (2009) eu trabalhei em um projeto como gerente de Q&A, e tive a oportunidade de colcoar em prática alguns conceitos. Entre eles, o de que o auditor de sistemas, buscando a qualidade, precisa ser um elemento motivador na equipe, de tal forma que conquiste a confiança dos programadores ao ponto que eles mesmos solicitem testes para seu código. Com esse pensamento, conseguimos recuperar a confiança de um cliente em um projeto que estava tentendo ao prejuízo, entregamos, e fornecemos um serviço de manutenção evolutiva e suporte com cinco integrantes na equipe. O cliente entendeu o coneito de qualidade, graças a um processo de comunicação ativo, e os programadores passaram a ter mais confiança em seus códigos após os testes e, um deles, terminou por receber um MVP da companhia. Assim, como você colou no seu post, os testes formais são uma excelente ferramenta, mas devem estar associados a antecipações e confiança dos desenvolvedores no setor de qualidade, o qual deve estar presente como ferramenta motivadora e não punidora em uma equipe de desenvolvimento. Parabéns pelo seu post!!