Agilidade X Formalismo

Sempre vimos o formalismo no desenvolvimento de software como um misto de desejo e desconfiança. Isto é explicável porque se por um lado ele melhora ou mesmo garante a qualidade de uma implementação de software, por outro lado ele costuma implicar em um custo muito alto, exigindo um tempo maior de desenvolvimento e o uso de profissionais com alto grau de formação.

A técnica de prova de corretude que aprendi na universidade foi a do uso da lógica de Hoare – o mesmo que criou o Quicksort, CSP e outros. Nesta técnica, Hoare nos ensinou que cada comando de nosso programa tem uma pré-condição e uma pós-condição que, em resumo, indicam a transformação exercida do comando em nosso ambiente em tempo de execução.

Outro conceito que levei algum tempo para compreender foi a ideia de “invariante”. Para poder indicar o que um loop deve fazer, Hoare nos pedia para definir o ponto-fixo do loop, garantindo que o loop iria convergir para a pós-condição pós-loop.

Complicado? Bem, fica a minha dica para vocês darem uma olhada no vídeo abaixo do time de pesquisa do RiSE. Fica muito mais simples quando temos uma ferramenta de apoio.

Para mim, projetos como este, ou como o Pex e Qex (ambos ferramentas que geram testes a partir de código, seja uma classe ou função, seja uma query SQL), são uma clara indicação de que logo será possível conciliar o desenvolvimento ágil com o rigor formal e o baixo custo.

Se isto acontecer, finalmente poderemos usar sem constrangimentos o termo Engenharia de Software. Sem o cálculo da corretude, ao meu ver, ficamos ainda desmerecedor do termo. Vocês não acham?

PS.: Me desculpem este um mês de ausência, mas as férias me chamavam e não pude resistir. Um grande 2010 para todos!